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

6 files changed, 14 insertions, 14 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 58ad1f00f..63a2c03a7 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -183,7 +183,7 @@ let declare_constant ?(internal = UserVerbose) id (cd,kind) =
 (** Declaration of inductive blocks *)
 
 let declare_inductive_argument_scopes kn mie =
-  list_iter_i (fun i {mind_entry_consnames=lc} ->
+  List.iter_i (fun i {mind_entry_consnames=lc} ->
     Notation.declare_ref_arguments_scope (IndRef (kn,i));
     for j=1 to List.length lc do
       Notation.declare_ref_arguments_scope (ConstructRef ((kn,i),j));
diff --git a/library/heads.ml b/library/heads.ml
index c86a91cc9..f3bcba770 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -113,8 +113,8 @@ let kind_of_head env t =
           k+n-m,[],a
         else
           (* enough arguments to [cst] *)
-          k,list_skipn n l,List.nth l (i-1) in
-      let l' = list_tabulate (fun _ -> mkMeta 0) q @ rest in
+          k,List.skipn n l,List.nth l (i-1) in
+      let l' = List.tabulate (fun _ -> mkMeta 0) q @ rest in
       aux k' l' a (with_subcase or with_case)
   | ConstructorHead when with_case -> NotImmediatelyComputableHead
   | x -> x
diff --git a/library/impargs.ml b/library/impargs.ml
index cd6365289..baf2e30ec 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -338,7 +338,7 @@ let set_manual_implicits env flags enriching autoimps l =
 	else l, None
     with Not_found -> l, None
   in
-  if not (list_distinct l) then
+  if not (List.distinct l) then
     error ("Some parameters are referred more than once.");
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
@@ -435,7 +435,7 @@ let compute_global_implicits flags manual = function
 (* Merge a manual explicitation with an implicit_status list *)
 
 let merge_impls (cond,oldimpls) (_,newimpls) =
-  let oldimpls,usersuffiximpls = list_chop (List.length newimpls) oldimpls in
+  let oldimpls,usersuffiximpls = List.chop (List.length newimpls) oldimpls in
   cond, (List.map2 (fun orig ni ->
     match orig with
     | Some (_, Manual, _) -> orig
@@ -482,7 +482,7 @@ let subst_implicits_decl subst (r,imps as o) =
   let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
 
 let subst_implicits (subst,(req,l)) =
-  (ImplLocal,list_smartmap (subst_implicits_decl subst) l)
+  (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
   List.rev_map
@@ -563,7 +563,7 @@ let rebuild_implicits (req,l) =
 	  if flags.auto then
 	    let newimpls = List.hd (compute_global_implicits flags [] ref) in
 	    let p = List.length (snd newimpls) - userimplsize in
-	    let newimpls = on_snd (list_firstn p) newimpls in
+	    let newimpls = on_snd (List.firstn p) newimpls in
 	    [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
 	  else
 	    [ref,oldimpls]
diff --git a/library/lib.ml b/library/lib.ml
index 907d251e7..a8a9f0c26 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -48,7 +48,7 @@ let subst_objects subst seg =
       if obj' == obj then node else
 	(id, obj')
   in
-    list_smartmap subst_one seg
+    List.smartmap subst_one seg
 
 (*let load_and_subst_objects i prefix subst seg =
   List.rev (List.fold_left (fun seg (id,obj as node) ->
diff --git a/library/libnames.ml b/library/libnames.ml
index 611cc9ad9..3555766f8 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -19,21 +19,21 @@ let pr_dirpath sl = (str (string_of_dirpath sl))
 
 (* Pop the last n module idents *)
 let pop_dirpath_n n dir =
-  make_dirpath (list_skipn n (repr_dirpath dir))
+  make_dirpath (List.skipn n (repr_dirpath dir))
 
 let pop_dirpath p = match repr_dirpath p with
   | [] -> anomaly "dirpath_prefix: empty dirpath"
   | _::l -> make_dirpath l
 
 let is_dirpath_prefix_of d1 d2 =
-  list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+  List.prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
 
 let chop_dirpath n d =
-  let d1,d2 = list_chop n (List.rev (repr_dirpath d)) in
+  let d1,d2 = List.chop n (List.rev (repr_dirpath d)) in
     make_dirpath (List.rev d1), make_dirpath (List.rev d2)
 
 let drop_dirpath_prefix d1 d2 =
-  let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
+  let d = Util.List.drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
     make_dirpath (List.rev d)
 
 let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1)
@@ -116,7 +116,7 @@ let pr_path sp = str (string_of_path sp)
 
 let restrict_path n sp =
   let dir, s = repr_path sp in
-  let dir' = list_firstn n (repr_dirpath dir) in
+  let dir' = List.firstn n (repr_dirpath dir) in
   make_path (make_dirpath dir') s
 
 (*s qualified names *)
diff --git a/library/library.ml b/library/library.ml
index a82b50481..bca44726d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -598,7 +598,7 @@ let import_module export (loc,qid) =
 
 let check_coq_overwriting p id =
   let l = repr_dirpath p in
-  if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then
+  if not !Flags.boot && l <> [] && string_of_id (List.last l) = "Coq" then
     errorlabstrm ""
       (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^
       ": it starts with prefix \"Coq\" which is reserved for the Coq library."))