Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)

- This way, the Makefile.build gets shorter and simplier, with a few nasty
   hacks removed.
 - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep".
   Instead, we now use ocamldep -modules, and process its output via coqdep_boot.
   This ways, *.cm* of .ml4 are correctly located, even when some .ml files
   aren't generated yet.
 - There is no risk of editing the .ml of a .ml4 by mistake, since it is by
   default in a binary format (cf pr_o.cmo and variable READABLE_ML4).
   M-x next-error still open the right .ml4 at the right location.
 - mltop.byteml is now mltop.ml, while mltop.optml keeps its name
 - .ml of .ml4 are added to .gitignore

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

10 files changed, 177 insertions, 114 deletions

diff --git a/.gitignore b/.gitignore
index 8b735ec5a..e96978b4c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -37,39 +37,21 @@
 *.v.html
 revision
 TAGS
+.DS_Store
 bin/
+_build
+plugins/*/*_mod.ml
+myocamlbuild_config.ml
 config/Makefile
 config/coq_config.ml
-plugins/dp/dp_zenon.ml
 dev/ocamldebug-coq
-dev/ocamlweb-doc/lex.ml
-dev/ocamlweb-doc/syntax.ml
-dev/ocamlweb-doc/syntax.mli
-ide/config_lexer.ml
-ide/config_parser.ml
-ide/config_parser.mli
-ide/coq_lex.ml
-ide/extract_index.ml
-ide/find_phrase.ml
-ide/highlight.ml
-ide/undo.mli
-ide/utf8_convert.ml
-kernel/byterun/coq_jumptbl.h
+plugins/micromega/csdpcert
 kernel/byterun/dllcoqrun.so
-kernel/copcodes.ml
-scripts/tolink.ml
 states/initial.coq
-theories/Numbers/Natural/BigN/NMake_gen.v
-tools/coqdep_lexer.ml
-tools/coqdoc/index.ml
-tools/coqdoc/cpretty.ml
-tools/coqwc.ml
-tools/gallina_lexer.ml
-toplevel/mltop.optml
-plugins/micromega/csdpcert
-toplevel/mltop.byteml
 coqdoc.sty
-ide/index_urls.txt
+
+# documentation
+
 doc/faq/html/
 doc/refman/Reference-Manual.pdf
 doc/refman/Reference-Manual.ps
@@ -96,7 +78,91 @@ doc/RecTutorial/RecTutorial.html
 doc/RecTutorial/RecTutorial.pdf
 doc/RecTutorial/RecTutorial.ps
 dev/doc/naming-conventions.pdf
-_build
-plugins/*/*_mod.ml
-myocamlbuild_config.ml
-.DS_Store
+
+# .mll files
+
+dev/ocamlweb-doc/lex.ml
+ide/coq_lex.ml
+ide/config_lexer.ml
+ide/utf8_convert.ml
+ide/highlight.ml
+plugins/dp/dp_zenon.ml
+tools/gallina_lexer.ml
+tools/coqwc.ml
+tools/coqdep_lexer.ml
+tools/coqdoc/index.ml
+tools/coqdoc/cpretty.ml
+
+# .mly files
+
+dev/ocamlweb-doc/syntax.ml
+dev/ocamlweb-doc/syntax.mli
+ide/config_parser.ml
+ide/config_parser.mli
+
+# .ml4 files
+
+lib/pp.ml
+lib/compat.ml
+lib/refutpat.ml
+parsing/g_xml.ml
+parsing/g_prim.ml
+parsing/q_util.ml
+parsing/tacextend.ml
+parsing/q_constr.ml
+parsing/g_vernac.ml
+parsing/pcoq.ml
+parsing/g_constr.ml
+parsing/g_ltac.ml
+parsing/vernacextend.ml
+parsing/g_tactic.ml
+parsing/argextend.ml
+parsing/g_decl_mode.ml
+parsing/q_coqast.ml
+parsing/g_proofs.ml
+parsing/lexer.ml
+plugins/xml/proofTree2Xml.ml
+plugins/xml/acic2Xml.ml
+plugins/xml/xml.ml
+plugins/xml/dumptree.ml
+plugins/xml/xmlentries.ml
+plugins/extraction/g_extraction.ml
+plugins/rtauto/g_rtauto.ml
+plugins/romega/g_romega.ml
+plugins/setoid_ring/newring.ml
+plugins/firstorder/g_ground.ml
+plugins/dp/g_dp.ml
+plugins/cc/g_congruence.ml
+plugins/ring/g_ring.ml
+plugins/field/field.ml
+plugins/funind/g_indfun.ml
+plugins/omega/g_omega.ml
+plugins/quote/g_quote.ml
+plugins/groebner/groebner.ml
+plugins/groebner/ideal.ml
+plugins/micromega/g_micromega.ml
+plugins/subtac/g_subtac.ml
+plugins/fourier/g_fourier.ml
+tactics/tauto.ml
+tactics/eauto.ml
+tactics/hipattern.ml
+tactics/class_tactics.ml
+tactics/rewrite.ml
+tactics/eqdecide.ml
+tactics/extratactics.ml
+tactics/extraargs.ml
+tools/coq_makefile.ml
+tools/coq_tex.ml
+toplevel/mltop.ml
+toplevel/whelp.ml
+
+# other auto-generated files
+
+ide/undo.mli
+toplevel/mltop.optml
+toplevel/mltop.byteml
+kernel/byterun/coq_jumptbl.h
+kernel/copcodes.ml
+scripts/tolink.ml
+theories/Numbers/Natural/BigN/NMake_gen.v
+ide/index_urls.txt
diff --git a/Makefile b/Makefile
index 2935c43da..a028359f0 100644
--- a/Makefile
+++ b/Makefile
@@ -234,8 +234,7 @@ optclean:
 clean-ide:
 	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
 	rm -f ide/input_method_lexer.ml
-	rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml
-	rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
+	rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
 	rm -f ide/utf8_convert.ml
 
 ml4clean:
diff --git a/Makefile.build b/Makefile.build
index fe69326d7..4303798ee 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -86,6 +86,12 @@ TIMECMD=	# is "'time -p'" to get compilation time of .v
 
 BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
 
+ifdef READABLE_ML4
+ PR_O = pr_o.cmo
+else
+ PR_O =
+endif
+
 ###########################################################################
 # Infrastructure for the rest of the Makefile
 ###########################################################################
@@ -662,25 +668,23 @@ parsing/grammar.cma: | parsing/grammar.mllib.d
 
 # toplevel/mltop.ml4 (ifdef Byte)
 
-toplevel/mltop.cmo: toplevel/mltop.byteml | toplevel/mltop.ml4.ml.d toplevel/mltop.ml4.d
-	$(SHOW)'OCAMLC    $<'	
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $< -o $@
+## NB: mltop.ml correspond to the byte version (and hence need no special rules)
+## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d
+## as dependency file, be sure to import the same modules in the different sections
+## of the ml4
 
-toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mltop.ml4.d
-	$(SHOW)'OCAMLOPT  $<'	
+toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d
+	$(SHOW)'OCAMLOPT    $<'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@
 
-## This works dependency-wise because the dependencies of the
-## .{opt,byte}ml files are those we deduce from the .ml4 file.
-## In other words, the Byte-only code doesn't import a new module.
-toplevel/mltop.byteml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
-	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \
+toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` \
 	  -DByte -DHasDynlink -impl $< $(TOTARGET)
 
-toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here 
-	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \
+toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
+	$(SHOW)'CAMLP4O   $<'
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` \
 	  $(NATDYNLINKDEF) -impl $< $(TOTARGET)
 
 # pretty printing of the revision number when compiling a checked out
@@ -750,25 +754,6 @@ checker/%.cmi: checker/%.mli | checker/%.mli.d
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
 
-ifdef KEEP_ML4_PREPROCESSED
-.PRECIOUS: %.ml4-preprocessed
-%.cmo: %.ml4-preprocessed | %.ml4.ml.d
-	$(SHOW)'OCAMLC    $<'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c -impl $<
-
-%.cmx: %.ml4-preprocessed | %.ml4.ml.d
-	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $<
-else
-%.cmo: %.ml4 | %.ml4.ml.d %.ml4.d
-	$(SHOW)'OCAMLC4   $<'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
-
-%.cmx: %.ml4 | %.ml4.ml.d %.ml4.d
-	$(SHOW)'OCAMLOPT4 $<'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
-endif
-
 %.cmo: %.ml | %.ml.d
 	$(SHOW)'OCAMLC    $<'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -808,9 +793,9 @@ plugins/%_mod.ml: plugins/%.mllib
 
 .SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
 
-%.ml4-preprocessed: %.ml4 | %.ml4.d
+%.ml: %.ml4 | %.ml4.d
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET)
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET)
 
 %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC      $<'
@@ -833,58 +818,49 @@ ifdef NO_RECOMPILE_ML4
 else
   SEP:=
 endif
+
+# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware
+# of .ml4 files
+
+OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP)
+
 %.ml4.d: $(D_DEPEND_BEFORE_SRC) %.ml4
 	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)( printf "%s" '$*.cmo $*.cmx $*.ml4.ml.d $*.ml4-preprocessed: $(SEP)' && $(CAMLP4DEPS) "$<" ) $(TOTARGET)
-
-%.ml4.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml4 $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML) %.ml4.d
-#Critical section:
-# Nobody (in a make -j) should touch the .ml file here.
-	$(SHOW)'OCAMLDEP4 $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< -o $*.ml \
-	  || ( RV=$$?; rm -f "$*.ml"; exit $${RV} )
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml | sed '' $(TOTARGET)
-	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml
-#End critical section
-
-checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC)
+	$(HIDE)( printf "%s" '$*.ml: $(SEP)' && $(CAMLP4DEPS) "$<" ) $(TOTARGET)
+
+checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)
 
-checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
+checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) -slash $(LOCALCHKLIBS) "$<" $(TOTARGET)
 
-%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML)
+%.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
 
-%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILESML)
+%.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
-	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' $(TOTARGET)
+	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
 
-checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
+checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -slash -boot -I checker -c "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -slash -I checker -c "$<" $(TOTARGET)
 
-%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
+%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -slash -boot -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)
-
-## Veerry nasty hack to keep ocamldep happy
-%.ml: | %.ml4
-	$(SHOW)'TOUCH     $@'
-	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -slash -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash -boot "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash "$<" $(TOTARGET)
 
 %.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
 	$(SHOW)'CCDEP     $<'
 	$(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< $(TOTARGET)
 
-.SECONDARY: $(GENFILES)
+.SECONDARY: $(GENFILES) $(ML4FILESML)
 
 ###########################################################################
 # this sets up developper supporting stuff
diff --git a/Makefile.common b/Makefile.common
index de84aaefe..8a29988d5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -372,8 +372,8 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
 
 STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
   $(GENFILES) \
-  source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
-  $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
+  source-doc revision toplevel/mltop.ml toplevel/mltop.optml \
+  $(STAGE1_ML4:.ml4=.ml) %.o
 
 ifdef CM_STAGE1
  STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
@@ -402,7 +402,7 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   world install coqide coqide-files coq coqlib \
   coqlight states check init theories theories-light \
   $(DOC_TARGETS) $(VO_TARGETS) validate \
-  %.vo %.glob states/% install-% %.ml4-preprocessed \
+  %.vo %.glob states/% install-% \
   $(DOC_TARGET_PATTERNS)
 
 ifndef CM_STAGE1
diff --git a/Makefile.stage1 b/Makefile.stage1
index a60d388fc..b67118d01 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -19,10 +19,12 @@ include Makefile.build
 -include $(MLIFILES:.mli=.mli.d)
 .SECONDARY: $(MLIFILES:.mli=.mli.d)
 ##Depends upon the fact that all .ml4.d for stage1 files are empty
--include $(STAGE1_ML4:.ml4=.ml4.ml.d)
-.SECONDARY: $(STAGE1_ML4:.ml4=.ml4.ml.d)
+-include $(STAGE1_ML4:.ml4=.ml.d)
+.SECONDARY: $(STAGE1_ML4:.ml4=.ml.d)
 -include  $(CFILES:.c=.c.d)
 .SECONDARY: $(CFILES:.c=.c.d)
+-include $(MLLIBFILES:.mllib=.mllib.d)
+.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)
 
 .PHONY: stage1
 stage1: $(STAGE1)
diff --git a/Makefile.stage2 b/Makefile.stage2
index 8f3d4e8bf..a7ecddc13 100644
--- a/Makefile.stage2
+++ b/Makefile.stage2
@@ -13,14 +13,11 @@ include Makefile.doc
 .SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)
 -include $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d))
 .SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d))
--include $(ML4FILES:.ml4=.ml4.ml.d)
-.SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d)
+-include $(ML4FILES:.ml4=.ml.d)
+.SECONDARY: $(ML4FILES:.ml4=.ml.d)
 -include $(VFILES:.v=.v.d)
 .SECONDARY: $(VFILES:.v=.v.d)
 
-.PHONY: stage2
-stage2: world
-
 # For emacs: 
 # Local Variables: 
 # mode: makefile 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 4edfbc748..8ec6b886e 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pr_o.cmo pa_macro.cmo" i*)
-(* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with
- * ast-based camlp4 *)
+(*i camlp4use: "pa_macro.cmo" i*)
 
 (*i $Id$ i*)
 
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index b7f6ec250..2798e4af6 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -22,6 +22,8 @@ let rec parse = function
   | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
   | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
+  | "-mldep" :: ocamldep :: ll ->
+      option_mldep := Some ocamldep; option_c := true; parse ll
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 8756d864d..95c794ca7 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -26,6 +26,7 @@ let option_c = ref false
 let option_noglob = ref false
 let option_slash = ref false
 let option_natdynlk = ref true
+let option_mldep = ref None
 
 let norecdir_list = ref ([]:string list)
 
@@ -176,7 +177,22 @@ let depend_ML str =
 	(" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
-let traite_fichier_ML md ext =
+let soustraite_fichier_ML dep md ext =
+  try
+    let chan = open_process_in (dep^" -modules "^md^ext) in
+    let list = ocamldep_parse (Lexing.from_channel chan) in
+    let a_faire = ref "" in
+    let a_faire_opt = ref "" in
+    List.iter
+      (fun str ->
+	 let byte,opt = depend_ML str in
+	 a_faire := !a_faire ^ byte;
+	 a_faire_opt := !a_faire_opt ^ opt)
+      (List.rev list);
+    (!a_faire, !a_faire_opt)
+  with Sys_error _ -> ("","")
+
+let autotraite_fichier_ML md ext =
   try
     let chan = open_in (md ^ ext) in
     let buf = Lexing.from_channel chan in
@@ -201,6 +217,11 @@ let traite_fichier_ML md ext =
     (!a_faire, !a_faire_opt)
   with Sys_error _ -> ("","")
 
+let traite_fichier_ML md ext =
+  match !option_mldep with
+    | Some dep -> soustraite_fichier_ML dep md ext
+    | None -> autotraite_fichier_ML md ext
+
 let traite_fichier_mllib md ext =
   try
     let chan = open_in (md ^ ext) in
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 89eeed54a..74c556a7d 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -225,8 +225,10 @@ and qual_id = parse
 and mllib_list = parse
   | coq_ident { let s = String.uncapitalize (Lexing.lexeme lexbuf)
 		in s :: mllib_list lexbuf }
+  | "*predef*" { mllib_list lexbuf }
   | space+ { mllib_list lexbuf }
   | eof { [] }
 
-
-
+and ocamldep_parse = parse
+  | [^ ':' ]* ':' { mllib_list lexbuf }
+  | _ { [] }