diff options
| -rw-r--r-- | Makefile.build | 13 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 49 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mli | 23 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 2 |
4 files changed, 83 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build index 857cb3914..2c6e73c5a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -496,9 +496,18 @@ printers: $(DEBUGPRINTERS) tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) -# coqdep_boot : a basic version of coqdep, with almost no dependencies +# coqdep_boot : a basic version of coqdep, with almost no dependencies. -$(COQDEPBOOT): tools/coqdep_lexer.ml tools/coqdep_common.ml tools/coqdep_boot.ml +# Here it is important to mention .ml files instead of .cmo in order +# to avoid using implicit rules and hence .ml.d files that would need +# coqdep_boot. + +COQDEPBOOTSRC:= \ + tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ + tools/coqdep_common.mli tools/coqdep_common.ml \ + tools/coqdep_boot.ml + +$(COQDEPBOOT): $(COQDEPBOOTSRC) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I tools, unix) 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 |