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

10 files changed, 34 insertions, 34 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 94980b596..210dbb02b 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -455,7 +455,7 @@ let rec compact_constr (lg, subs as s) c k =
   match kind_of_term c with
       Rel i ->
         if i < k then c,s else
-          (try mkRel (k + lg - list_index (i-k+1) subs), (lg,subs)
+          (try mkRel (k + lg - List.index (i-k+1) subs), (lg,subs)
           with Not_found -> mkRel (k+lg), (lg+1, (i-k+1)::subs))
     | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
     | Evar(ev,v) ->
@@ -734,7 +734,7 @@ let rec get_args n tys f e stk =
           let eargs = Array.sub l n (na-n) in
           (Inl (subs_cons(args,e)), Zapp eargs :: s)
         else (* more lambdas *)
-          let etys = list_skipn na tys in
+          let etys = List.skipn na tys in
           get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 5f677d056..a2ce4f270 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -110,7 +110,7 @@ let subst_rel_declaration sub (id,copt,t as x) =
   let t' = subst_mps sub t in
   if copt == copt' & t == t' then x else (id,copt',t')
 
-let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
 (* TODO: these substitution functions could avoid duplicating things
    when the substitution have preserved all the fields *)
@@ -141,11 +141,11 @@ let hcons_rel_decl ((n,oc,t) as d) =
   and t' = hcons_types t
   in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
 
-let hcons_rel_context l = list_smartmap hcons_rel_decl l
+let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
 let hcons_polyarity ar =
   { poly_param_levels =
-      list_smartmap (Option.smartmap hcons_univ) ar.poly_param_levels;
+      List.smartmap (Option.smartmap hcons_univ) ar.poly_param_levels;
     poly_level = hcons_univ ar.poly_level }
 
 let hcons_const_type = function
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6c7f4408f..b93b9f19b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -351,7 +351,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
 let compute_rec_par (env,n,_,_) hyps nmr largs =
 if nmr = 0 then 0 else
 (* start from 0, hyps will be in reverse order *)
-  let (lpar,_) = list_chop nmr largs in
+  let (lpar,_) = List.chop nmr largs in
   let rec find k index =
       function
 	  ([],_) -> nmr
@@ -375,7 +375,7 @@ let abstract_mind_lc env ntyps npars lc =
     lc
   else
     let make_abs =
-      list_tabulate
+      List.tabulate
 	(function i -> lambda_implicit_lift npars (mkRel (i+1))) ntyps
     in
     Array.map (substl make_abs) lc
@@ -457,7 +457,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
     let auxnpar = mib.mind_nparams_rec in
     let nonrecpar = mib.mind_nparams - auxnpar in
     let (lpar,auxlargs) =
-      try list_chop auxnpar largs
+      try List.chop auxnpar largs
       with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
       (* If the inductive appears in the args (non params) then the
 	 definition is not positive. *)
@@ -539,7 +539,7 @@ let check_positivity kn env_ar params inds =
   let nmr = rel_context_nhyps params in
   let check_one i (_,lcnames,lc,(sign,_)) =
     let ra_env =
-      list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+      List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     let nargs = rel_context_nhyps sign - nmr in
     check_positivity_one ienv params (kn,i) nargs lcnames lc
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 58689a926..d86abb435 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,7 +54,7 @@ let inductive_params (mib,_) = mib.mind_nparams
 let ind_subst mind mib =
   let ntypes = mib.mind_ntypes in
   let make_Ik k = mkInd (mind,ntypes-k-1) in
-  list_tabulate make_Ik ntypes
+  List.tabulate make_Ik ntypes
 
 (* Instantiate inductives in constructor type *)
 let constructor_instantiate mind mib c =
@@ -272,7 +272,7 @@ let extended_rel_list n hyps =
   reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   applist
     (mkInd ind,
        List.map (lift mip.mind_nrealargs_ctxt) params
@@ -327,7 +327,7 @@ let build_branches_type ind (_,mip as specif) params p =
     let (args,ccl) = decompose_prod_assum typi in
     let nargs = rel_context_length args in
     let (_,allargs) = decompose_app ccl in
-    let (lparams,vargs) = list_chop (inductive_params specif) allargs in
+    let (lparams,vargs) = List.chop (inductive_params specif) allargs in
     let cargs =
       let cstr = ith_constructor_of_inductive ind (i+1) in
       let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
@@ -344,7 +344,7 @@ let build_case_type n p c realargs =
 let type_case_branches env (ind,largs) pj c =
   let specif = lookup_mind_specif env ind in
   let nparams = inductive_params specif in
-  let (params,realargs) = list_chop nparams largs in
+  let (params,realargs) = List.chop nparams largs in
   let p = pj.uj_val in
   let univ = is_correct_arity env c pj ind specif params in
   let lc = build_branches_type ind specif params p in
@@ -451,7 +451,7 @@ let push_var renv (x,ty,spec) =
     genv = spec:: renv.genv }
 
 let assign_var_spec renv (i,spec) =
-  { renv with genv = list_assign renv.genv (i-1) spec }
+  { renv with genv = List.assign renv.genv (i-1) spec }
 
 let push_var_renv renv (x,ty) =
   push_var renv (x,ty,lazy Not_subterm)
@@ -521,7 +521,7 @@ let branches_specif renv c_spec ci =
 		    vra
 	      | Dead_code -> Array.create nca Dead_code
 	      | _ -> Array.create nca Not_subterm) in
-	 list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+	 List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
       car 
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
@@ -870,7 +870,7 @@ let check_one_cofix env nbfix def deftype =
             let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
-            let realargs = list_skipn mib.mind_nparams args in
+            let realargs = List.skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
               | (t::lr), (rar::lrar) ->
                   if rar = mk_norec then
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5eddb6c84..19075058a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -562,7 +562,7 @@ and clean_expr l = function
        if  str_clean == str && sig_clean = sigt.typ_expr then
 	 s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
   | SEBstruct str as s->
-      let str_clean = Util.list_smartmap (clean_struct l) str in 
+      let str_clean = Util.List.smartmap (clean_struct l) str in 
 	if  str_clean == str then s else SEBstruct(str_clean)
   |  str -> str 
 
@@ -572,7 +572,7 @@ let rec collect_mbid l = function
 	if  str_clean == str then s else 
       SEBfunctor (mbid,sigt,str_clean)
   | SEBstruct str as s->
-      let str_clean = Util.list_smartmap (clean_struct l) str in 
+      let str_clean = Util.List.smartmap (clean_struct l) str in 
 	if  str_clean == str then s else SEBstruct(str_clean)
   |  _ -> anomaly "Modops:the evaluation of the structure failed "
        
diff --git a/kernel/names.ml b/kernel/names.ml
index d7b9516ae..aa5313842 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -369,7 +369,7 @@ module Hdir = Hashcons.Make(
   struct
     type t = dir_path
     type u = identifier -> identifier
-    let hash_sub hident d = list_smartmap hident d
+    let hash_sub hident d = List.smartmap hident d
     let rec equal d1 d2 =
       (d1==d2) ||
       match (d1,d2) with
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 3d2f19aac..476a92bed 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -93,8 +93,8 @@ let lookup_rel_val n env =
 
 let env_of_rel n env =
   { env with
-    env_rel_context = Util.list_skipn n env.env_rel_context;
-    env_rel_val = Util.list_skipn n env.env_rel_val;
+    env_rel_context = Util.List.skipn n env.env_rel_context;
+    env_rel_val = Util.List.skipn n env.env_rel_val;
     env_nb_rel = env.env_nb_rel - n
   }
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index a654bc04d..269f7a5d9 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -34,7 +34,7 @@ let rec lookup_named id = function
   | [] -> raise Not_found
 
 let named_context_length = List.length
-let named_context_equal = list_equal eq_named_declaration
+let named_context_equal = List.equal eq_named_declaration
 
 let vars_of_named_context = List.map (fun (id,_,_) -> id)
 
@@ -61,7 +61,7 @@ let map_context f l =
       if body_o' == body_o && typ' == typ then decl else
 	(n, body_o', typ')
   in
-    list_smartmap map_decl l
+    List.smartmap map_decl l
 
 let map_rel_context = map_context
 let map_named_context = map_context
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 5fec0c2c7..c590a5101 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -198,7 +198,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     check (fun mib ->
       let nparamdecls = List.length mib.mind_params_ctxt in
       let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
-      snd (list_chop nparamdecls names))
+      snd (List.chop nparamdecls names))
       (fun x -> RecordProjectionsExpected x);
   end;
   (* we first check simple things *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1f864926a..9334a06d1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -130,12 +130,12 @@ let sup u v =
 	if UniverseLevel.equal u v then Atom u else Max ([u;v],[])
     | u, Max ([],[]) -> u
     | Max ([],[]), v -> v
-    | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
-    | Max (gel,gtl), Atom v -> Max (list_add_set v gel,gtl)
+    | Atom u, Max (gel,gtl) -> Max (List.add_set u gel,gtl)
+    | Max (gel,gtl), Atom v -> Max (List.add_set v gel,gtl)
     | Max (gel,gtl), Max (gel',gtl') ->
-	let gel'' = list_union gel gel' in
-	let gtl'' = list_union gtl gtl' in
-	Max (list_subtract gel'' gtl'',gtl'')
+	let gel'' = List.union gel gel' in
+	let gtl'' = List.union gtl gtl' in
+	Max (List.subtract gel'' gtl'',gtl'')
 
 (* Comparison on this type is pointer equality *)
 type canonical_arc =
@@ -423,7 +423,7 @@ let merge g arcu arcv =
                  (* redirected to it *)
 	let redirect (g,w,w') arcv =
  	  let g' = enter_equiv_arc arcv.univ arcu.univ g in
- 	  (g',list_unionq arcv.lt w,arcv.le@w')
+ 	  (g',List.unionq arcv.lt w,arcv.le@w')
 	in
 	let (g',w,w') = List.fold_left redirect (g,[],[]) v in
 	let g_arcu = (g',arcu) in
@@ -759,7 +759,7 @@ let make_max = function
 
 let remove_large_constraint u = function
   | Atom u' as x -> if u = u' then Max ([],[]) else x
-  | Max (le,lt) -> make_max (list_remove u le,lt)
+  | Max (le,lt) -> make_max (List.remove u le,lt)
 
 let is_direct_constraint u = function
   | Atom u' -> u = u'
@@ -900,8 +900,8 @@ module Huniv =
 	match u, v with
 	  | Atom u, Atom v -> u == v
 	  | Max (gel,gtl), Max (gel',gtl') ->
-	      (list_for_all2eq (==) gel gel') &&
-              (list_for_all2eq (==) gtl gtl')
+	      (List.for_all2eq (==) gel gel') &&
+              (List.for_all2eq (==) gtl gtl')
 	  | _ -> false
       let hash = Hashtbl.hash
     end)
@@ -928,7 +928,7 @@ module Hconstraints =
       let hash_sub huc s =
 	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
       let equal s s' =
-	list_for_all2eq (==)
+	List.for_all2eq (==)
 	  (Constraint.elements s)
 	  (Constraint.elements s')
       let hash = Hashtbl.hash