Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48

11 files changed, 46 insertions, 295 deletions

diff --git a/Makefile.common b/Makefile.common
index 32bf19e99c..780ba717ee 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -42,17 +42,17 @@ COQTIME_FILE_MAKER:=tools/TimeFileMaker.py
 COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
 COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
 VOTOUR:=bin/votour
+OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
+OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE)
 
 # these get installed!
 TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
-	$(COQWORKMGR) $(COQPP) $(VOTOUR)
+	$(COQWORKMGR) $(COQPP) $(VOTOUR) $(OCAMLLIBDEP)
 TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
 	$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)
 
 COQDEPBOOT:=bin/coqdep_boot$(EXE)
 COQDEPBOOTBYTE:=bin/coqdep_boot.byte$(EXE)
-OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
-OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE)
 FAKEIDE:=bin/fake_ide$(EXE)
 FAKEIDEBYTE:=bin/fake_ide.byte$(EXE)
 
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e5edd08995..3d1fc6d4b9 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -545,7 +545,7 @@ Computing Module dependencies
 In order to compute module dependencies (to be used by ``make`` or
 ``dune``), |Coq| provides the ``coqdep`` tool.
 
-``coqdep`` computes inter-module dependencies for |Coq| and |OCaml|
+``coqdep`` computes inter-module dependencies for |Coq|
 programs, and prints the dependencies on the standard output in a
 format readable by make. When a directory is given as argument, it is
 recursively looked at.
@@ -554,11 +554,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require``
 commands (``Require``, ``Require Export``, ``Require Import``), but also at the
 command ``Declare ML Module``.
 
-Dependencies of |OCaml| modules are computed by looking at
-`open` commands and the dot notation *module.value*. However, this is
-done approximately and you are advised to use ``ocamldep`` instead for the
-|OCaml| module dependencies.
-
 See the man page of ``coqdep`` for more details and options.
 
 Both Dune and ``coq_makefile`` use ``coqdep`` to compute the
diff --git a/man/coqdep.1 b/man/coqdep.1
index 4223482c99..0770ce88c8 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -12,9 +12,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs
 .BI \-coqlib \ directory
 ]
 [
-.BI \-c
-]
-[
 .BI \-i
 ]
 [
@@ -52,10 +49,6 @@ directives and the dot notation
 .SH OPTIONS
 
 .TP
-.BI \-c
-Prints the dependencies of Caml modules.
-(On Caml modules, the behaviour is exactly the same as ocamldep).
-.TP
 .BI \-f \ file
 Read filenames and options -I, -R and -Q from a _CoqProject FILE.
 .TP 
@@ -152,29 +145,8 @@ example% coqdep \-I . *.v
 .fi
 .RE
 .br
-.ne 7
-.LP
-To get only the Caml dependencies:
-.IP
-.B
-example% coqdep \-c \-I . *.ml
-.RS
-.sp .5
-.nf
-.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo
-.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx
-.B C.cmo: C.ml
-.B C.cmx: C.ml
-.B B.cmo: B.ml
-.B B.cmx: B.ml
-.B A.cmo: A.ml
-.B A.cmx: A.ml
-.fi
-.RE
-.br
-.ne 7
 
 .SH BUGS
 
 Please report any bug to
-.B coq\-bugs@pauillac.inria.fr
+.B https://github.com/coq/coq/issues
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index d3ed5e78b4..49fb88cd8c 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -91,6 +91,7 @@ COQDEP   ?= "$(COQBIN)coqdep"
 COQDOC   ?= "$(COQBIN)coqdoc"
 COQPP    ?= "$(COQBIN)coqpp"
 COQMKFILE ?= "$(COQBIN)coq_makefile"
+OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep"
 
 # Timing scripts
 COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
@@ -455,13 +456,13 @@ all.ps: $(VFILES)
 	$(SHOW)'COQDOC -ps $(GAL)'
 	$(HIDE)$(COQDOC) \
 		-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
-		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+		-o $@ `$(COQDEP) -sort $(VFILES)`
 
 all.pdf: $(VFILES)
 	$(SHOW)'COQDOC -pdf $(GAL)'
 	$(HIDE)$(COQDOC) \
 		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
-		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+		-o $@ `$(COQDEP) -sort $(VFILES)`
 
 # FIXME: not quite right, since the output name is different
 gallinahtml: GAL=-g
@@ -747,12 +748,12 @@ $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
 	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
 
 $(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
-	$(SHOW)'COQDEP $<'
-	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+	$(SHOW)'OCAMLLIBDEP $<'
+	$(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok)
 
 $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
-	$(SHOW)'COQDEP $<'
-	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+	$(SHOW)'OCAMLLIBDEP $<'
+	$(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok)
 
 # If this makefile is created using a _CoqProject we have coqdep get
 # options from it. This avoids argument length limits for pathological
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 950c784325..a96173c057 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -31,7 +31,6 @@ let option_sort = ref false
 let usage () =
   eprintf " usage: coqdep [options] <filename>+\n";
   eprintf " options:\n";
-  eprintf "  -c : Also print the dependencies of caml modules (=ocamldep).\n";
   eprintf "  -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n";
   eprintf "  -sort : output the given file name ordered by dependencies\n";
   eprintf "  -noglob | -no-glob : \n";
@@ -44,8 +43,6 @@ let usage () =
   eprintf "  -vos : also output dependencies about .vos files\n";
   eprintf "  -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n";
   eprintf "  -coqlib dir : set the coq standard library directory\n";
-  eprintf "  -suffix s : \n";
-  eprintf "  -slash : deprecated, no effect\n";
   eprintf "  -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
   exit 1
 
@@ -65,8 +62,6 @@ let treat_coqproject f =
   iter_sourced (fun f -> treat_file None f) (all_files project)
 
 let rec parse = function
-  (* TODO, deprecate option -c *)
-  | "-c" :: ll -> option_c := true; parse ll
   | "-boot" :: ll -> option_boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | "-vos" :: ll -> write_vos := true; parse ll
@@ -81,8 +76,6 @@ let rec parse = function
   | "-exclude-dir" :: [] -> usage ()
   | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll
   | "-coqlib" :: [] -> usage ()
-  | "-suffix" :: s :: ll -> suffixe := s ; parse ll
-  | "-suffix" :: [] -> usage ()
   | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
   | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
   | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
@@ -114,11 +107,7 @@ let coqdep () =
       (Envars.xdg_dirs ~warn:(fun x -> coqdep_warning "%s" x));
     List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath;
   end;
-  List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu;
-  List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu;
-  List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu;
   if !option_sort then begin sort (); exit 0 end;
-  if !option_c then mL_dependencies ();
   coq_dependencies ();
   ()
 
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 5ece595f13..683165f026 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -31,15 +31,12 @@ module StrListMap = Map.Make(StrList)
 
 type dynlink = Opt | Byte | Both | No | Variable
 
-let option_c = ref false
 let option_noglob = ref false
 let option_dynlink = ref Both
 let option_boot = ref false
 
 let norec_dirs = ref StrSet.empty
 
-let suffixe = ref ".vo"
-
 type dir = string option
 
 (** [get_extension f l] checks whether [f] has one of the extensions
@@ -58,18 +55,6 @@ let basename_noext filename =
   let fn = Filename.basename filename in
   try Filename.chop_extension fn with Invalid_argument _ -> fn
 
-(** ML Files specified on the command line. In the entries:
-    - the first string is the basename of the file, without extension nor
-      directory part
-    - the second string of [mlAccu] is the extension (either .ml or .mlg)
-    - the [dir] part is the directory, with None used as the current directory
-*)
-
-let mlAccu  = ref ([] : (string * string * dir) list)
-and mliAccu = ref ([] : (string * dir) list)
-and mllibAccu = ref ([] : (string * dir) list)
-and mlpackAccu = ref ([] : (string * dir) list)
-
 (** Coq files specifies on the command line:
     - first string is the full filename, with only its extension removed
     - second string is the absolute version of the previous (via getcwd)
@@ -125,8 +110,6 @@ let mkknown () =
     with Not_found -> None
   in add, iter, search
 
-let add_ml_known, _, search_ml_known = mkknown ()
-let add_mli_known, _, search_mli_known = mkknown ()
 let add_mllib_known, _, search_mllib_known = mkknown ()
 let add_mlpack_known, _, search_mlpack_known = mkknown ()
 
@@ -231,64 +214,6 @@ let file_name s = function
   | None     -> s
   | Some d   -> d // s
 
-let depend_ML str =
-  match search_mli_known str, search_ml_known str with
-    | Some mlidir, Some mldir ->
-        let mlifile = file_name str mlidir
-        and mlfile = file_name str mldir in
-        (" "^mlifile^".cmi"," "^mlfile^".cmx")
-    | None, Some mldir ->
-        let mlfile = file_name str mldir in
-        (" "^mlfile^".cmo"," "^mlfile^".cmx")
-    | Some mlidir, None ->
-        let mlifile = file_name str mlidir in
-        (" "^mlifile^".cmi"," "^mlifile^".cmi")
-    | None, None -> "", ""
-
-let traite_fichier_ML md ext =
-  try
-    let chan = open_in (md ^ ext) in
-    let buf = Lexing.from_channel chan in
-    let deja_vu = ref (StrSet.singleton md) in
-    let a_faire = ref "" in
-    let a_faire_opt = ref "" in
-    begin try
-      while true do
-        let (Use_module str) = caml_action buf in
-        if StrSet.mem str !deja_vu then
-          ()
-        else begin
-          deja_vu := StrSet.add str !deja_vu;
-          let byte,opt = depend_ML str in
-          a_faire := !a_faire ^ byte;
-          a_faire_opt := !a_faire_opt ^ opt
-        end
-      done
-    with Fin_fichier -> ()
-    end;
-    close_in chan;
-    (!a_faire, !a_faire_opt)
-  with Sys_error _ -> ("","")
-
-let traite_fichier_modules md ext =
-  try
-    let chan = open_in (md ^ ext) in
-    let list = mllib_list (Lexing.from_channel chan) in
-    List.fold_left
-      (fun a_faire str -> match search_mlpack_known str with
-        | Some mldir ->
-          let file = file_name str mldir in
-          a_faire @ [file]
-        | None ->
-          match search_ml_known str with
-            | Some mldir ->
-              let file = file_name str mldir in
-                    a_faire @ [file]
-            | None -> a_faire) [] list
-  with
-    | Sys_error _ -> []
-    | Syntax_error (i,j) -> error_cannot_parse (md^ext) (i,j)
-
 (* Makefile's escaping rules are awful: $ is escaped by doubling and
    other special characters are escaped by backslash prefixing while
    backslashes themselves must be escaped only if part of a sequence
@@ -418,10 +343,7 @@ let rec find_dependencies basename =
                   | None ->
                     match search_mlpack_known s with
                   | Some mldir -> declare ".cmo" mldir s
-                  | None ->
-                    match search_ml_known s with
-                      | Some mldir -> declare ".cmo" mldir s
-                      | None -> warning_declare f str
+                  | None -> warning_declare f str
                 end
                 in
               List.iter decl sl
@@ -449,59 +371,16 @@ let rec find_dependencies basename =
   with Sys_error _ -> [] (* TODO: report an error? *)
 
 
-let mL_dependencies () =
-  List.iter
-    (fun (name,ext,dirname) ->
-       let fullname = file_name name dirname in
-       let (dep,dep_opt) = traite_fichier_ML fullname ext in
-       let intf = match search_mli_known name with
-         | None -> ""
-         | Some mldir -> " "^(file_name name mldir)^".cmi"
-       in
-       let efullname = escape fullname in
-       printf "%s.cmo:%s%s\n" efullname dep intf;
-       printf "%s.cmx:%s%s\n%!" efullname dep_opt intf)
-    (List.rev !mlAccu);
-  List.iter
-    (fun (name,dirname) ->
-       let fullname = file_name name dirname in
-       let (dep,_) = traite_fichier_ML fullname ".mli" in
-       printf "%s.cmi:%s\n%!" (escape fullname) dep)
-    (List.rev !mliAccu);
-  List.iter
-    (fun (name,dirname) ->
-       let fullname = file_name name dirname in
-       let dep = traite_fichier_modules fullname ".mllib" in
-       let efullname = escape fullname in
-       printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
-       printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname;
-       printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n%!" efullname efullname)
-    (List.rev !mllibAccu);
-  List.iter
-    (fun (name,dirname) ->
-       let fullname = file_name name dirname in
-       let dep = traite_fichier_modules fullname ".mlpack" in
-       let efullname = escape fullname in
-       printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname (String.concat " " dep);
-       printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
-       printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname;
-       let efullname_capital = String.capitalize_ascii (Filename.basename efullname) in
-       List.iter (fun dep ->
-         printf "%s.cmx : FOR_PACK=-for-pack %s\n" dep efullname_capital)
-         dep;
-       printf "%!")
-    (List.rev !mlpackAccu)
-
 let write_vos = ref false
 
 let coq_dependencies () =
   List.iter
     (fun (name,_) ->
        let ename = escape name in
-       let glob = if !option_noglob then "" else " "^ename^".glob" in
+       let glob = if !option_noglob then "" else ename^".glob " in
        let deps = find_dependencies name in
-       printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename
-        (string_of_dependency_list !suffixe deps);
+       printf "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename
+        (string_of_dependency_list ".vo" deps);
        printf "%s.vio: %s.v %s\n" ename ename
          (string_of_dependency_list ".vio" deps);
        if !write_vos then
@@ -517,10 +396,8 @@ let rec suffixes = function
 
 let add_caml_known phys_dir _ f =
   let basename,suff =
-    get_extension f [".ml";".mli";".mlg";".mllib";".mlpack"] in
+    get_extension f [".mllib"; ".mlpack"] in
   match suff with
-    | ".ml"|".mlg" -> add_ml_known basename (Some phys_dir) suff
-    | ".mli" -> add_mli_known basename (Some phys_dir) suff
     | ".mllib" -> add_mllib_known basename (Some phys_dir) suff
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
     | _ -> ()
@@ -605,18 +482,15 @@ let rec treat_file old_dirname old_name =
            in
            Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
     | S_REG ->
-        (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with
-           | (base,".v") ->
-               let name = file_name base dirname
-               and absname = absolute_file_name base dirname in
-               addQueue vAccu (name, absname)
-           | (base,(".ml"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname)
-           | (base,".mli") -> addQueue mliAccu (base,dirname)
-           | (base,".mllib") -> addQueue mllibAccu (base,dirname)
-           | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
-           | _ -> ())
+      (match get_extension name [".v"] with
+       | base,".v" ->
+         let name = file_name base dirname
+         and absname = absolute_file_name base dirname in
+         addQueue vAccu (name, absname)
+       | _ -> ())
     | _ -> ()
 
+(* "[sort]" outputs `.v` files required by others *)
 let sort () =
   let seen = Hashtbl.create 97 in
   let rec loop file =
@@ -639,7 +513,7 @@ let sort () =
         done
       with Fin_fichier ->
         close_in cin;
-        printf "%s%s " file !suffixe
+        printf "%s.v " file
     end
   in
   List.iter (fun (name,_) -> loop name) !vAccu
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 1820db4a1e..aca68cc780 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -21,11 +21,9 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a
 val find_dir_logpath: string -> string list
 
 (** Options *)
-val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
 val write_vos : bool ref
-val suffixe : string ref
 
 type dynlink = Opt | Byte | Both | No | Variable
 val option_dynlink : dynlink ref
@@ -36,18 +34,11 @@ type dir = string option
 val treat_file : dir -> string -> unit
 
 (** ML-related manipulation *)
-val mlAccu : (string * string * dir) list ref
-val mliAccu : (string * dir) list ref
-val mllibAccu : (string * dir) list ref
-val add_ml_known : string -> dir -> string -> unit
-val add_mli_known : string -> dir -> string -> unit
-val add_mllib_known : string -> dir -> string -> unit
-val mL_dependencies : unit -> unit
-
 val coq_dependencies : unit -> unit
 val add_known : bool -> string -> string list -> string -> unit
 val add_coqlib_known : bool -> string -> string list -> string -> unit
 
+(* Used to locate plugins for [Declare ML Module] *)
 val add_caml_dir : string -> unit
 
 (** Simply add this directory and imports it, no subdirs. This is used
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index 018fc1b7a2..24452f203a 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -8,12 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type mL_token = Use_module of string
-
 type qualid = string list
 
 type coq_token =
-    Require of qualid option * qualid list
+  | Require of qualid option * qualid list
   | Declare of string list
   | Load of string
   | AddLoadPath of string
@@ -23,6 +21,3 @@ exception Fin_fichier
 exception Syntax_error of int * int
 
 val coq_action : Lexing.lexbuf -> coq_token
-val caml_action : Lexing.lexbuf -> mL_token
-val mllib_list : Lexing.lexbuf -> string list
-val ocamldep_parse : Lexing.lexbuf -> string list
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 743da535b8..157c2b7dba 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -13,8 +13,6 @@
   open Filename
   open Lexing
 
-  type mL_token = Use_module of string
-
   type qualid = string list
 
   type coq_token =
@@ -152,56 +150,6 @@ and add_loadpath_as path = parse
   | dot
       { AddLoadPath path }
 
-and caml_action = parse
-  | space +
-      { caml_action lexbuf }
-  | "open" space* (caml_up_ident as id)
-        { Use_module (String.uncapitalize_ascii id) }
-  | "module" space+ caml_up_ident
-        { caml_action lexbuf }
-  | caml_low_ident { caml_action lexbuf }
-  | caml_up_ident
-      { qual_id (Lexing.lexeme lexbuf) lexbuf }
-  | ['0'-'9']+
-    | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
-    | '0' ['o' 'O'] ['0'-'7']+
-    | '0' ['b' 'B'] ['0'-'1']+
-      { caml_action lexbuf }
-  | ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)?
-      { caml_action lexbuf }
-  | "\""
-      { string lexbuf; caml_action lexbuf }
-  | "'" [^ '\\' '\''] "'"
-      { caml_action lexbuf }
-  | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'"
-      { caml_action lexbuf }
-  | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
-      { caml_action lexbuf }
-  | "(*"
-      { comment lexbuf; caml_action lexbuf }
-  | "#" | "&"  | "&&" | "'" | "(" | ")" | "*" | "," | "?" | "->" | "." | ".."
-   | ".(" | ".[" | ":" | "::" | ":=" | ";" | ";;" | "<-" | "=" | "[" | "[|"
-   | "[<" | "]" | "_" | "{" | "|" | "||" | "|]" | ">]" | "}" | "!=" | "-"
-   | "-."    { caml_action lexbuf }
-
-  | ['!' '?' '~']
-    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
-            { caml_action lexbuf }
-  | ['=' '<' '>' '@' '^' '|' '&' '$']
-    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
-            { caml_action lexbuf }
-  | ['+' '-']
-    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
-            { caml_action lexbuf }
-  | "**"
-    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
-            { caml_action lexbuf }
-  | ['*' '/' '%']
-    ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~'] *
-            { caml_action lexbuf }
-  | eof { raise Fin_fichier }
-  | _ { caml_action lexbuf }
-
 and comment = parse
   | "(*"
       { comment lexbuf; comment lexbuf }
@@ -218,20 +166,6 @@ and comment = parse
   | _
       { comment lexbuf }
 
-and string = parse
-  | '"' (* '"' *)
-      { () }
-  | '\\' ("\010" | "\013" | "\010\013") [' ' '\009'] *
-      { string lexbuf }
-  | '\\' ['\\' '"' 'n' 't' 'b' 'r'] (*'"'*)
-      { string lexbuf }
-  | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9']
-      { string lexbuf }
-  | eof
-      { raise Fin_fichier }
-  | _
-      { string lexbuf }
-
 and load_file = parse
   | '"' [^ '"']* '"' (*'"'*)
       { let s = lexeme lexbuf in
@@ -320,20 +254,3 @@ and modules mllist = parse
       { syntax_error lexbuf }
   | _
       { Declare (List.rev mllist) }
-
-and qual_id ml_module_name = parse
-  | '.' [^ '.' '(' '[']
-      { Use_module (String.uncapitalize_ascii ml_module_name) }
-  | eof { raise Fin_fichier }
-  | _ { caml_action lexbuf }
-
-and mllib_list = parse
-  | caml_up_ident { let s = String.uncapitalize_ascii (Lexing.lexeme lexbuf)
-		in s :: mllib_list lexbuf }
-  | "*predef*" { mllib_list lexbuf }
-  | space+ { mllib_list lexbuf }
-  | eof { [] }
-  | _ { syntax_error lexbuf }
-
-and ocamldep_parse = parse
-  | [^ ':' ]* ':' { mllib_list lexbuf }
diff --git a/tools/dune b/tools/dune
index 204bd09535..c0e4e20f72 100644
--- a/tools/dune
+++ b/tools/dune
@@ -29,7 +29,15 @@
  (modules coqdep_lexer coqdep_common coqdep)
  (libraries coq.lib))
 
-(ocamllex coqdep_lexer)
+; Bare-bones mllib/mlpack parser
+(executable
+ (name ocamllibdep)
+ (public_name ocamllibdep)
+ (modules ocamllibdep)
+ (package coq)
+ (libraries unix))
+
+(ocamllex coqdep_lexer ocamllibdep)
 
 (executable
  (name coqwc)
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 41a4e2a86a..2ecc20f1b0 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -195,6 +195,14 @@ let mllib_dependencies () =
        flush stdout)
     (List.rev !mllibAccu)
 
+let coq_makefile_mode = ref false
+
+let print_for_pack modname d =
+  if !coq_makefile_mode then
+    printf "%s.cmx : FOR_PACK=-for-pack %s\n" d modname
+  else
+    printf "%s_FORPACK:= -for-pack %s\n" d modname
+
 let mlpack_dependencies () =
   List.iter
     (fun (name,dirname) ->
@@ -204,7 +212,7 @@ let mlpack_dependencies () =
        let sdeps = String.concat " " deps in
        let efullname = escape fullname in
        printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname sdeps;
-       List.iter (fun d -> printf "%s_FORPACK:= -for-pack %s\n" d modname) deps;
+       List.iter (print_for_pack modname) deps;
        printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n"
          efullname efullname;
        printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n"
@@ -213,6 +221,7 @@ let mlpack_dependencies () =
     (List.rev !mlpackAccu)
 
 let rec parse = function
+  | "-c" :: r -> coq_makefile_mode := true; parse r
   | "-I" :: r :: ll ->
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)