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 ++++----
 scripts/coqc.ml4 | 2 +-
 2 files changed, 5 insertions(+), 5 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
diff --git a/scripts/coqc.ml4 b/scripts/coqc.ml4
index a1d64c1d25..c4d6468dd7 100644
--- a/scripts/coqc.ml4
+++ b/scripts/coqc.ml4
@@ -111,7 +111,7 @@ let parse_args () =
     | "-t" :: rem -> 
 	keep := true ; parse (cfiles,args) rem
     | "-bindir" :: d :: rem ->
-	bindir := d ; parse (cfiles,d::"-bindir"::args) rem
+	bindir := d ; parse (cfiles,args) rem
     | "-bindir" :: []       ->
 	usage ()
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-- 
cgit v1.2.3