following changes in lambdapi, rename --erasing into --mapping

Deducteam · Jan 21, 2025 · 7eb6a02 · 7eb6a02
1 parent f6a2d21
commit 7eb6a02
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Makefile b/Makefile
@@ -242,7 +242,7 @@ endif
 
 %.v: %.lp
 	@echo lambdapi export -o stt_coq $<
-	@lambdapi export -o stt_coq --encoding $(HOL2DK_DIR)/encoding.lp --renaming $(HOL2DK_DIR)/renaming.lp --erasing $(MAPPING) --use-notations --requiring "$(REQUIRING)" $< > $@
+	@lambdapi export -o stt_coq --encoding $(HOL2DK_DIR)/encoding.lp --renaming $(HOL2DK_DIR)/renaming.lp --mapping $(MAPPING) --use-notations --requiring "$(REQUIRING)" $< > $@
 
 .PHONY: clean-v
 clean-v: rm-v clean-vo

diff --git a/README.md b/README.md
@@ -191,7 +191,7 @@ Translating HOL-Light proofs to Lambdapi and Coq
 ------------------------------------------------
 
 **Requirements:**
-- lambdapi commit >= c24b28e2 (28/11/24) > 2.5.1
+- lambdapi commit >= 21ee7f3d (21/01/25)
 - coq >= 8.19
 - [coq-hol-light-real-with-N](https://github.com/Deducteam/coq-hol-light-real-with-N)
 - [coq-fourcolor-reals](https://github.com/coq-community/fourcolor/blob/master/coq-fourcolor-reals.opam)