Commit c7fc192e authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

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.
parent 0e83b784
...@@ -978,6 +978,11 @@ depend: $(COQVD) ...@@ -978,6 +978,11 @@ depend: $(COQVD)
clean:: clean::
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) 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 else
drivers/coq-realizations.aux: drivers/coq-realizations.aux:
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