Maintenant on scan les .ml pour les .dot/.dep.ps (fait avec Matthias).

Rien de fait pour les .ml4 encore. De plus il y a une bizarrerie avec 
contradiction.ml qui plante sur coqdoc, ce n'est pas très grave, mais il 
faudra regarder un jour quand même...



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

1 files changed, 19 insertions, 18 deletions

diff --git a/Makefile.build b/Makefile.build
index 8f1d5601f8..5388b20b00 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -990,32 +990,33 @@ devel: $(DEBUGPRINTERS)
 %.dep.ps: %.dot
 	$(DOT) $(DOTOPTS) -o $@ $<
 
-kernel/kernel.dot: $(KERNELMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(KERNELMLI)
+kernel/kernel.dot: $(KERNEL)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(KERNEL:.cmo=.ml)) 
 
-interp/interp.dot: $(INTERPMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(INTERPMLI)
+interp/interp.dot: $(INTERP)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(INTERP:.cmo=.ml)) 
 
-pretyping/pretyping.dot: $(PRETYPINGMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(PRETYPINGMLI)
+pretyping/pretyping.dot: $(PRETYPING)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(PRETYPING:.cmo=.ml)) 
 
-library/library.dot: $(LIBRARYMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(LIBRARYMLI)
+library/library.dot: $(LIBRARY)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(LIBRARY:.cmo=.ml))
 
-parsing/parsing.dot: $(PARSINGMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(PARSINGMLI)
+parsing/parsing.dot: $(PARSING) $(HIGHPARSING)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(PARSING:.cmo=.ml)) $(wildcard $(HIGHPARSING:.cmo=.ml)) 
 
-tactics/tactics.dot: $(TACTICSMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(TACTICSMLI)
+tactics/tactics.dot: $(TACTICS) $(HIGHTACTICS)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(TACTICS:.cmo=.ml)) $(wildcard $(HIGHTACTICS:.cmo=.ml))
 
-proofs/proofs.dot: $(PROOFSMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(PROOFSMLI)
+proofs/proofs.dot: $(PROOFS)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(PROOFS:.cmo=.ml))
 
-toplevel/toplevel.dot: $(TOPLEVELMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(TOPLEVELMLI)
+toplevel/toplevel.dot: $(TOPLEVEL)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(TOPLEVEL:.cmo=.ml))
 
-coq.dot: $(LIBREP:.cmo=.cmi) $(COQMLI:.mli=.cmi)
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(LIBREP:.cmo=.mli)) $(COQMLI)
+COQCMO:=$(LIBREP) $(KERNEL) $(INTERP) $(PRETYPING) $(LIBRARY) $(PARSING) $(HIGHPARSING) $(TACTICS) $(HIGHTACTICS) $(PROOFS) $(TOPLEVEL)
+coq.dot: $(COQCMO)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(wildcard $(COQCMO:.cmo=.ml))
 
 
 # For emacs: