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

1 files changed, 0 insertions, 2 deletions

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