avoid dependency nightmare by creating coqdep_{lexer,common}.mli

 Sequel to commit 14476 : in fact, even with "tools" in .PHONY,
 we still may have coqdep stuff being recompiled in a "make"
 that follows a successful "make". This seems to related to
 the hacks I've introduced to prevent ocamlopt from erasing
 and recreating .cmi when there's no .mli around
 (cf. comment around line 823 in Makefile.build).

 Scenario:
  - First we build coqdep_boot directly out of coqdep_lexer.ml and co.
    When ocamlopt is around, this creates some .cmx and .cmi,
    but no .cmo.
  - Later we build coqdep, which need coqdep_lexer.cmx and co.
    Now "make" checks whether these .cmx are up-to-date.
    But our hacks made these .cmx depend on the corresponding .cmi.
    Then "make" checks whether these .cmi are up-to-date.
    But our hacks made these .cmi depend on the corresponding .cmo.
    These .cmo doesn't exist yet, we run ocamlc, which recreates
    the .cmi with same content but a different timestamp.
    For some strange reason, even with refreshed .cmi, the .cmx
    are not remade by this run, but will be on the next run.

 Conclusion: what a mess. Implicit rules about .cmx / .cmo / .cmi
 should be improved, but I see currently no simple solution.

 In the meantime, an simple ad-hoc fix is to create these two .mli ...

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

3 files changed, 72 insertions, 2 deletions

diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
new file mode 100644
index 000000000..53c3ba17c
--- /dev/null
+++ b/tools/coqdep_common.mli
@@ -0,0 +1,49 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val option_c : bool ref
+val option_noglob : bool ref
+val option_slash : bool ref
+val option_natdynlk : bool ref
+val option_mldep : string option ref
+val norecdir_list : string list ref
+val suffixe : string ref
+type dir = string option
+val ( // ) : string -> string -> string
+val get_extension : string -> string list -> string * string
+val basename_noext : string -> string
+val mlAccu : (string * string * dir) list ref
+val mliAccu : (string * dir) list ref
+val mllibAccu : (string * dir) list ref
+val vAccu : (string * string) list ref
+val addQueue : 'a list ref -> 'a -> unit
+val add_ml_known : string -> dir -> unit
+val iter_ml_known : (string -> dir -> unit) -> unit
+val search_ml_known : string -> dir option
+val add_mli_known : string -> dir -> unit
+val iter_mli_known : (string -> dir -> unit) -> unit
+val search_mli_known : string -> dir option
+val add_mllib_known : string -> dir -> unit
+val search_mllib_known : string -> dir option
+val vKnown : (string list, string) Hashtbl.t
+val coqlibKnown : (string list, unit) Hashtbl.t
+val file_name : string -> string option -> string
+val escape : string -> string
+val canonize : string -> string
+val mL_dependencies : unit -> unit
+val coq_dependencies : unit -> unit
+val suffixes : 'a list -> 'a list list
+val add_known : string -> string list -> string -> unit
+val add_directory :
+  bool ->
+  (string -> string list -> string -> unit) -> string -> string list -> unit
+val add_dir :
+  (string -> string list -> string -> unit) -> string -> string list -> unit
+val add_rec_dir :
+  (string -> string list -> string -> unit) -> string -> string list -> unit
+val treat_file : dir -> string -> unit
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
new file mode 100644
index 000000000..260586270
--- /dev/null
+++ b/tools/coqdep_lexer.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type mL_token = Use_module of string
+
+type coq_token =
+    Require of string list list
+  | RequireString of string
+  | Declare of string list
+  | Load of string
+
+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 09433ff76..e0bf1daec 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -13,8 +13,6 @@
 
   type mL_token = Use_module of string
 
-  type spec = bool
-
   type coq_token =
     | Require of string list list
     | RequireString of string