Commit fc927c12 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make sure that the Why3 library is visible from the plugin, since it references WhyType.

parent 4dcb456d
......@@ -795,12 +795,12 @@ src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 $< && \
WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 $< && \
WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......@@ -1432,10 +1432,10 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte -R lib/coq-tactic Why3 bench/coq-tactic/test.v
$(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
$(COQC) -opt -R lib/coq-tactic Why3 bench/coq-tactic/test.v
$(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
......
Require Import ZArith Reals Why3.BuiltIn.
Declare ML Module "why3tac".
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