diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coqProject_file.ml | 7 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 1 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/flags.mli | 4 | ||||
| -rw-r--r-- | lib/lib.mllib | 2 | ||||
| -rw-r--r-- | lib/system.ml | 4 |
6 files changed, 9 insertions, 13 deletions
diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index c2bcd73fff..d0b01453a0 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -29,6 +29,7 @@ type project = { v_files : string sourced list; mli_files : string sourced list; ml4_files : string sourced list; + mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; mlpack_files : string sourced list; @@ -66,6 +67,7 @@ let mk_project project_file makefile install_kind use_ocamlopt = { v_files = []; mli_files = []; ml4_files = []; + mlg_files = []; ml_files = []; mllib_files = []; mlpack_files = []; @@ -223,6 +225,7 @@ let process_cmd_line orig_dir proj args = { proj with v_files = proj.v_files @ [sourced f] } | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] } | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } @@ -249,9 +252,9 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; -let all_files { v_files; ml_files; mli_files; ml4_files; +let all_files { v_files; ml_files; mli_files; ml4_files; mlg_files; mllib_files; mlpack_files } = - v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + v_files @ mli_files @ ml4_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files let map_sourced_list f l = List.map (fun x -> f x.thing) l ;; diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 5780bb5d78..2a6a09a9a0 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -23,6 +23,7 @@ type project = { v_files : string sourced list; mli_files : string sourced list; ml4_files : string sourced list; + mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; mlpack_files : string sourced list; diff --git a/lib/flags.ml b/lib/flags.ml index c8f19f2f11..582506f3a8 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -103,10 +103,6 @@ let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = !auto_intros -let universe_polymorphism = ref false -let make_universe_polymorphism b = universe_polymorphism := b -let is_universe_polymorphism () = !universe_polymorphism - let polymorphic_inductive_cumulativity = ref false let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity diff --git a/lib/flags.mli b/lib/flags.mli index 3d9eafde75..b667235678 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -84,10 +84,6 @@ val is_auto_intros : unit -> bool val program_mode : bool ref val is_program_mode : unit -> bool -(** Global universe polymorphism flag. *) -val make_universe_polymorphism : bool -> unit -val is_universe_polymorphism : unit -> bool - (** Global polymorphic inductive cumulativity flag. *) val make_polymorphic_inductive_cumulativity : bool -> unit val is_polymorphic_inductive_cumulativity : unit -> bool diff --git a/lib/lib.mllib b/lib/lib.mllib index 41b3622a99..206b2504db 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,5 +1,3 @@ -Coq_config - Hook Flags Control diff --git a/lib/system.ml b/lib/system.ml index eec007dcab..a9db95318f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -83,7 +83,9 @@ let file_exists_respecting_case path f = let rec aux f = let bf = Filename.basename f in let df = Filename.dirname f in - (String.equal df "." || aux df) + (* When [df] is the same as [f], it means that the root of the file system + has been reached. There is no point in looking further up. *) + (String.equal df "." || String.equal f df || aux df) && exists_in_dir_respecting_case (Filename.concat path df) bf in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f |