- Make .vo files depend on coqdoc if COQ_XML is set (bug #848)

 - Clean up NO_RECOMPILE_LIB treatment a bit
 - Clean up .vo dependencies in general


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9478 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 24 deletions

diff --git a/Makefile b/Makefile
index bf642dd7f3..e280327356 100644
--- a/Makefile
+++ b/Makefile
@@ -620,11 +620,7 @@ beforedepend:: ide/utf8_convert.ml
 
 COQIDEVO=ide/utf8.vo
 
-ifdef NO_RECOMPILE_LIB
- $(COQIDEVO): | states/initial.coq
-else
- $(COQIDEVO): states/initial.coq
-endif
+$(COQIDEVO): states/initial.coq $(VO_TOOLS_DEP)
 	$(BOOTCOQTOP) -compile $*
 
 IDEFILES=$(COQIDEVO) ide/utf8.v ide/coq.png ide/.coqide-gtk2rc
@@ -1090,12 +1086,6 @@ CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \
 	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO)
 
-ifdef NO_RECOMPILE_LIB
- $(CONTRIBVO): | states/initial.coq
-else
- $(CONTRIBVO): states/initial.coq
-endif
-
 contrib: $(CONTRIBVO) $(CONTRIBCMO)
 omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
 ring: $(RINGVO) $(RINGCMO)
@@ -1119,27 +1109,27 @@ ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO)
 
 SYNTAXPP=syntax/PPConstr.v syntax/PPCases.v
 
-states/initial.coq: states/MakeInitial.v $(INITVO)
-	$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
-
 ifdef NO_RECOMPILE_LIB
- theories/Init/%.vo: theories/Init/%.v | $(BESTCOQTOP)
-else
- theories/Init/%.vo: $(BESTCOQTOP) theories/Init/%.v
+ VO_TOOLS_DEP += |
+endif
+ VO_TOOLS_DEP += $(BESTCOQTOP)
+ifdef COQ_XML
+ VO_TOOLS_DEP += $(COQDOC)
 endif
+
+states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_DEP)
+	$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq
+
+theories/Init/%.vo: theories/Init/%.v $(VO_TOOLS_DEP)
 	$(BOOTCOQTOP) -nois -compile theories/Init/$*
 
-ifdef NO_RECOMPILE_LIB
- theories/%.vo: theories/%.v | states/initial.coq
-else
- theories/%.vo: theories/%.v states/initial.coq
-endif
+theories/%.vo: theories/%.v states/initial.coq $(VO_TOOLS_DEP)
 	$(BOOTCOQTOP) -compile theories/$*
 
-contrib/%.vo: contrib/%.v
+contrib/%.vo: contrib/%.v states/initial.coq $(VO_TOOLS_DEP)
 	$(BOOTCOQTOP) -compile contrib/$*
 
-contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC)
+contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(VO_TOOLS_DEP)
 	$(BOOTCOQTOP) -is states/barestate.coq -compile $*
 
 cleantheories: