Skip to content

GitLab

Commit db532aa5 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files
Options

Ensure that BuiltIn.vo is built before Why3.vo since the tactic uses some of its definitions.

parent a38c5a55
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 2 deletions
Makefile.in
View file @ db532aa5
......@@ -793,12 +793,12 @@ src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(if $(QUIET),@echo 'Camlp5 $<' &&) \
$(CAMLP5O) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
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
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
touch src/coq-tactic/.why3-vo-opt
......
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