aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/check.ml')
-rw-r--r--checker/check.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 9e6b63537..5b58dc9ba 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -149,20 +149,20 @@ let canonical_path_name p =
let find_logical_path phys_dir =
let phys_dir = canonical_path_name phys_dir in
- match list_filter2 (fun p d -> p = phys_dir) !load_paths with
+ match List.filter2 (fun p d -> p = phys_dir) !load_paths with
| _,[dir] -> dir
| _,[] -> default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
let remove_load_path dir =
- load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+ load_paths := List.filter2 (fun p d -> p <> dir) !load_paths
let add_load_path (phys_path,coq_path) =
if !Flags.debug then
ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
str phys_path);
let phys_path = canonical_path_name phys_path in
- match list_filter2 (fun p d -> p = phys_path) !load_paths with
+ match List.filter2 (fun p d -> p = phys_path) !load_paths with
| _,[dir] ->
if coq_path <> dir
(* If this is not the default -I . to coqtop *)
@@ -185,7 +185,7 @@ let add_load_path (phys_path,coq_path) =
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
let load_paths_of_dir_path dir =
- fst (list_filter2 (fun p d -> d = dir) !load_paths)
+ fst (List.filter2 (fun p d -> d = dir) !load_paths)
(************************************************************************)
(*s Locate absolute or partially qualified library names in the path *)