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

4 files changed, 9 insertions, 9 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f99d8c109..190181c23 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -460,8 +460,8 @@ let pr pr sep inherited a =
         pr spc ltop b),
       lletin
   | CAppExpl (_,(Some i,f),l) ->
-      let l1,l2 = list_chop i l in
-      let c,l1 = list_sep_last l1 in
+      let l1,l2 = List.chop i l in
+      let c,l1 = List.sep_last l1 in
       let p = pr_proj (pr mt) pr_appexpl c f l1 in
       if l2<>[] then
 	p ++ prlist (pr spc (lapp,L)) l2, lapp
@@ -473,8 +473,8 @@ let pr pr sep inherited a =
       hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg
   | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
   | CApp (_,(Some i,f),l) ->
-      let l1,l2 = list_chop i l in
-      let c,l1 = list_sep_last l1 in
+      let l1,l2 = List.chop i l in
+      let c,l1 = List.sep_last l1 in
       assert (snd c = None);
       let p = pr_proj (pr mt) pr_app (fst c) f l1 in
       if l2<>[] then
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7118388cb..1a8f71397 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -592,7 +592,7 @@ let pr_fix_tac (id,n,c) =
   let rec set_nth_name avoid n = function
       (nal,ty)::bll ->
         if n <= List.length nal then
-          match list_chop (n-1) nal with
+          match List.chop (n-1) nal with
               _, (_,Name id) :: _ -> id, (nal,ty)::bll
             | bef, (loc,Anonymous) :: aft ->
                 let id = next_ident_away (id_of_string"y") avoid in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 86b2da2eb..7fbbc0a2e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -93,7 +93,7 @@ let print_impargs_by_name max = function
 let print_one_impargs_list l =
   let imps = List.filter is_status_implicit l in
   let maximps = List.filter Impargs.maximal_insertion_of imps in
-  let nonmaximps = list_subtract imps maximps in
+  let nonmaximps = List.subtract imps maximps in
   print_impargs_by_name false nonmaximps @
   print_impargs_by_name true maximps
 
@@ -127,7 +127,7 @@ let need_expansion impl ref =
   let ctx = (prod_assum typ) in
   let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
   impl <> [] & List.length impl >= nprods &
-    let _,lastimpl = list_chop nprods impl in
+    let _,lastimpl = List.chop nprods impl in
       List.filter is_status_implicit lastimpl <> []
 
 let print_impargs ref =
diff --git a/printing/printer.ml b/printing/printer.ml
index 70a90b8ea..1ad9dba49 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -289,7 +289,7 @@ let pr_concl n sigma g =
 (* display evar type: a context and a type *)
 let pr_evgl_sign gl =
   let ps = pr_named_context_of (evar_unfiltered_env gl) in
-  let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
+  let _,l = List.filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
   let ids = List.rev (List.map pi1 l) in
   let warn =
     if ids = [] then mt () else
@@ -664,7 +664,7 @@ let print_one_inductive env mib ((_,i) as ind) =
   brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
 
 let print_mutual_inductive env mind mib =
-  let inds = list_tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
+  let inds = List.tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
   in
   hov 0 (
     str (if mib.mind_finite then "Inductive " else "CoInductive ") ++