diff options
Diffstat (limited to 'tools/coqdep_boot.ml')
| -rw-r--r-- | tools/coqdep_boot.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index bcc9f33f..bc3435a6 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <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 *) @@ -16,7 +16,6 @@ open Coqdep_common *) let rec parse = function - | "-slash" :: ll -> option_slash := true; parse ll | "-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 *) @@ -25,20 +24,26 @@ let rec parse = function | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) - add_dir add_known r []; + 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 - add_rec_dir add_known "." [] + 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 () |