aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index afc8101e14..d8e9142ab4 100644
--- a/Makefile
+++ b/Makefile
@@ -198,15 +198,15 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \
theories/Init/Logic_TypeSyntax.vo
theories/Init/%.vo: theories/Init/%.v states/barestate.coq
- $(COQC) -q -I theories/Init -is states/barestate.coq $<
+ $(COQC) -bindir $(COQTOP) -q -I theories/Init -is states/barestate.coq $<
TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo
tactics/%.vo: tactics/%.v states/barestate.coq
- $(COQC) -q -I tactics -is states/barestate.coq $<
+ $(COQC) -bindir $(COQTOP) -q -I tactics -is states/barestate.coq $<
states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO)
- ./coqtop.byte -q -batch -silent -is states/barestate.coq -I tactics -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
+ ./coqtop.byte -q -batch -silent -is states/barestate.coq -I tactics -I theories/Init -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
clean::
rm -f states/barestate.coq states/initial.coq
@@ -447,7 +447,7 @@ toplevel/mltop.cmx: toplevel/mltop.ml4
$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
.v.vo:
- $(COQC) $(COQINCLUDES) -q $<
+ $(COQC) -bindir $(COQTOP) -I states $(COQINCLUDES) -q $<
.el.elc:
echo "(setq load-path (cons \".\" load-path))" > $*.compile