From c5471cf03d2d6aa2ba6ed9e2ce015aab1e45f536 Mon Sep 17 00:00:00 2001
From: courant
Date: Fri, 21 Apr 2000 08:50:21 +0000
Subject: Compilation pbs (coqc not finding coqtop, coqc not finding .vo when
 building states, coqc wrongly giving option -bindir to coqtop) fixed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@365 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Makefile')

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
-- 
cgit v1.2.3