aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorHugo Herbelin2015-02-16 08:32:15 +0100
committerHugo Herbelin2015-02-16 12:31:59 +0100
commit48d611ff2a60131369a66924e8d54f8e7c4ad911 (patch)
treeeabf646b2270ff42df0ba804c204e4a36a218ee3 /tools
parentaf53b96fd5363150a47bec97f74b2b3159368ed3 (diff)
Using home-made ocamllibdep rather than coqdep_boot.
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep_boot.ml51
1 files changed, 0 insertions, 51 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
deleted file mode 100644
index bc3435a644..0000000000
--- a/tools/coqdep_boot.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Coqdep_common
-
-(** [coqdep_boot] is a stripped-down version of [coqdep], whose
- behavior is the one of [coqdep -boot]. Its only dependencies
- are [Coqdep_lexer], [Coqdep_common] and [Unix], and it should stay so.
- If it needs someday some additional information, pass it via
- options (see for instance [option_natdynlk] below).
-*)
-
-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 *)
- add_caml_dir r;
- norec_dirs:=r::!norec_dirs;
- parse ll
- | f :: ll -> treat_file None f; parse ll
- | [] -> ()
-
-let coqdep_boot () =
- let () = option_boot := true in
- if Array.length Sys.argv < 2 then exit 1;
- parse (List.tl (Array.to_list Sys.argv));
- if !option_c then begin
- add_rec_dir add_known "." [];
- add_rec_dir (fun _ -> add_caml_known) "." ["Coq"];
- end
- else begin
- add_rec_dir add_known "theories" ["Coq"];
- add_rec_dir add_known "plugins" ["Coq"];
- add_caml_dir "tactics";
- add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
- add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
- end;
- if !option_c then mL_dependencies ();
- coq_dependencies ()
-
-let _ = Printexc.catch coqdep_boot ()