Moving Utils.list_* to a proper CList module, which includes stdlib

List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7

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 *)