Skip to content

GitLab

Commit 6181e14e authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Make Coq realization regeneration dependent on the driver file.

parent 54f46f3b
Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
Makefile.in
View file @ 6181e14e
...@@ -978,7 +978,7 @@ depend: $(COQVD) ...@@ -978,7 +978,7 @@ depend: $(COQVD)
clean:: clean::
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
update-coq: bin/why3 update-coq: bin/why3 drivers/coq-realizations.aux
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_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_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 #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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment