From 7eb6a02574b86d06a2cefb00c0d09ea44d0ffba0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 21 Jan 2025 14:40:39 +0100 Subject: [PATCH] following changes in lambdapi, rename --erasing into --mapping --- Makefile | 2 +- README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 45bb1ad..b34809d 100644 --- 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 index 755cce5..0c80856 100644 --- 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)