From c7fc192e1f35b46c74c6c72c49e5d9e67a0550fd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 24 Feb 2012 21:30:54 +0100 Subject: [PATCH] Add a rule to regenerate Coq realizations. Note: Currently, only the set of real theories has been fully converted to the new script format. So it is the only one enabled. The other ones would not survive the process. --- Makefile.in | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Makefile.in b/Makefile.in index 0003cd8e5..66bc135ae 100644 --- a/Makefile.in +++ b/Makefile.in @@ -978,6 +978,11 @@ depend: $(COQVD) clean:: rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) +update-coq: bin/why3 + #for f in $(COQLIBS_INT_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done + for f in $(COQLIBS_REAL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done + #for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done + else drivers/coq-realizations.aux: -- GitLab