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

21 files changed, 124 insertions, 124 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 163675dfb3..196f5a0e7e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -98,7 +98,7 @@ let msg_may_need_inversion () =
 
 (* Utils *)
 let make_anonymous_patvars n =
-  list_make n (PatVar (Loc.ghost,Anonymous))
+  List.make n (PatVar (Loc.ghost,Anonymous))
 
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
@@ -295,7 +295,7 @@ let try_find_ind env sigma typ realnames =
   let names =
     match realnames with
       | Some names -> names
-      | None -> list_make (List.length realargs) Anonymous in
+      | None -> List.make (List.length realargs) Anonymous in
   IsInd (typ,ind,names)
 
 let inh_coerce_to_ind evdref env ty tyi =
@@ -515,7 +515,7 @@ let mk_dep_patt_row (pats,_,eqn) =
 
 let dependencies_in_pure_rhs nargs eqns =
   if eqns = [] && not (Flags.is_program_mode ()) then
-    list_make nargs false (* Only "_" patts *) else
+    List.make nargs false (* Only "_" patts *) else
   let deps_rows = List.map mk_dep_patt_row eqns in
   let deps_columns = matrix_transpose deps_rows in
   List.map (List.exists ((=) true)) deps_columns
@@ -531,7 +531,7 @@ let rec dep_in_tomatch n = function
 
 let dependencies_in_rhs nargs current tms eqns =
   match kind_of_term current with
-  | Rel n when dep_in_tomatch n tms -> list_make nargs true
+  | Rel n when dep_in_tomatch n tms -> List.make nargs true
   | _ -> dependencies_in_pure_rhs nargs eqns
 
 (* Computing the matrix of dependencies *)
@@ -551,7 +551,7 @@ let rec find_dependency_list tmblock = function
   | (used,tdeps,d)::rest ->
       let deps = find_dependency_list tmblock rest in
       if used && List.exists (fun x -> dependent_decl x d) tmblock
-      then list_add_set (List.length rest + 1) (list_union deps tdeps)
+      then List.add_set (List.length rest + 1) (List.union deps tdeps)
       else deps
 
 let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist =
@@ -680,7 +680,7 @@ let merge_name get_name obj = function
 let merge_names get_name = List.map2 (merge_name get_name)
 
 let get_names env sign eqns =
-  let names1 = list_make (List.length sign) Anonymous in
+  let names1 = List.make (List.length sign) Anonymous in
   (* If any, we prefer names used in pats, from top to bottom *)
   let names2,aliasname =
     List.fold_right
@@ -691,7 +691,7 @@ let get_names env sign eqns =
   (* Otherwise, we take names from the parameters of the constructor but
      avoiding conflicts with user ids *)
   let allvars =
-    List.fold_left (fun l (_,_,eqn) -> list_union l eqn.rhs.avoid_ids)
+    List.fold_left (fun l (_,_,eqn) -> List.union l eqn.rhs.avoid_ids)
       [] eqns in
   let names3,_ =
     List.fold_left2
@@ -723,7 +723,7 @@ let push_rels_eqn sign eqn =
      rhs = {eqn.rhs with rhs_env = push_rel_context sign eqn.rhs.rhs_env} }
 
 let push_rels_eqn_with_names sign eqn =
-  let subpats = List.rev (list_firstn (List.length sign) eqn.patterns) in
+  let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
   let subpatnames = List.map alias_of_pat subpats in
   let sign = recover_initial_subpattern_names subpatnames sign in
   push_rels_eqn sign eqn
@@ -1134,7 +1134,7 @@ let build_branch current realargs deps (realnames,curname) pb arsign eqns const_
   (* We adjust the terms to match in the context they will be once the *)
   (* context [x1:T1,..,xn:Tn] will have been pushed on the current env *)
   let typs' =
-    list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
+    List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
 
   let extenv = push_rel_context typs pb.env in
 
@@ -1462,7 +1462,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
     | Evar ev ->
         let ty = get_type_of env sigma t in
         let inst =
-	  list_map_i
+	  List.map_i
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
@@ -1477,7 +1477,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       let ty = lift (-k) (aux x (get_type_of env !evdref t)) in
       let depvl = free_rels ty in
       let inst =
-	list_map_i
+	List.map_i
 	  (fun i _ -> if List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
       let rel_filter =
@@ -1534,15 +1534,15 @@ let build_inversion_problem loc env sigma tms t =
     | App (f,v) when isConstruct f ->
 	let cstr = destConstruct f in
 	let n = constructor_nrealargs env cstr in
-	let l = list_lastn n (Array.to_list v) in
-	let l,acc = list_fold_map' reveal_pattern l acc in
+	let l = List.lastn n (Array.to_list v) in
+	let l,acc = List.fold_map' reveal_pattern l acc in
 	PatCstr (Loc.ghost,cstr,l,Anonymous), acc
     | _ -> make_patvar t acc in
   let rec aux n env acc_sign tms acc =
     match tms with
     | [] -> [], acc_sign, acc
     | (t, IsInd (_,IndType(indf,realargs),_)) :: tms ->
-	let patl,acc = list_fold_map' reveal_pattern realargs acc in
+	let patl,acc = List.fold_map' reveal_pattern realargs acc in
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
 	let sign = make_arity_signature env true indf' in
@@ -1570,14 +1570,14 @@ let build_inversion_problem loc env sigma tms t =
   let n = List.length sign in
 
   let decls =
-    list_map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
+    List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
 
   let pb_env = push_rel_context sign env in
   let decls =
     List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
 
   let decls = List.rev decls in
-  let dep_sign = find_dependencies_signature (list_make n true) decls in
+  let dep_sign = find_dependencies_signature (List.make n true) decls in
 
   let sub_tms =
     List.map2 (fun deps (tm,(tmtyp,_),(na,b,t)) ->
@@ -1664,7 +1664,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		  if nrealargs_ctxt <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
-	      | None -> list_make nrealargs_ctxt Anonymous in
+	      | None -> List.make nrealargs_ctxt Anonymous in
 	  (na,None,build_dependent_inductive env0 indf')
 	  ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
   let rec buildrec n = function
@@ -2273,11 +2273,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
     
   let dep_sign =
     find_dependencies_signature
-      (list_make (List.length typs) true)
+      (List.make (List.length typs) true)
       typs in
     
   let typs' =
-    list_map3
+    List.map3
       (fun (tm,tmt) deps na ->
          let deps = if not (isRel tm) then [] else deps in
            ((tm,tmt),deps,na))
@@ -2346,11 +2346,11 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
 
     let dep_sign =
       find_dependencies_signature
-        (list_make (List.length typs) true)
+        (List.make (List.length typs) true)
         typs in
 
     let typs' =
-      list_map3
+      List.map3
         (fun (tm,tmt) deps na ->
           let deps = if not (isRel tm) then [] else deps in
           ((tm,tmt),deps,na))
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index fd88049b24..099a2ab76f 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -262,7 +262,7 @@ and cbv_stack_term info stack env t =
           let eargs = Array.sub args nlams (nargs-nlams) in
           cbv_stack_term info (APP(eargs,stk)) env' b
         else
-          let ctxt' = list_skipn nargs ctxt in
+          let ctxt' = List.skipn nargs ctxt in
           LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
 
     (* a Fix applied enough -> IOTA *)
@@ -328,7 +328,7 @@ and cbv_norm_value info = function (* reduction under binders *)
       map_constr_with_binders subs_lift (cbv_norm_term info) env t
   | LAM (n,ctxt,b,env) ->
       let nctxt =
-        list_map_i (fun i (x,ty) ->
+        List.map_i (fun i (x,ty) ->
           (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in
       compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b)
   | FIXP ((lij,(names,lty,bds)),env,args) ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a1b7e5e9dd..14476354b3 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -313,7 +313,7 @@ let add_coercion_in_graph (ic,source,target) =
              try_add_new_path1 (s,target) (p@[ic]);
              Gmap.iter
 	       (fun (u,v) q ->
-                  if u<>v & u = target &&  not (list_equal coe_info_typ_equal p q) then
+                  if u<>v & u = target &&  not (List.equal coe_info_typ_equal p q) then
 		    try_add_new_path1 (s,v) (p@[ic]@q))
                old_inheritance_graph
            end;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0b48654b69..0239a7e44d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -51,7 +51,7 @@ let apply_pattern_coercion loc pat p =
   List.fold_left
     (fun pat (co,n) ->
        let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
-	 Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+	 Glob_term.PatCstr (loc, co, List.tabulate f (n+1), Anonymous))
     pat p
 
 (* raise Not_found if no coercion found *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 50410ad825..d30c1a11fa 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -217,7 +217,7 @@ let lookup_index_as_renamed env t n =
 
 let update_name na ((_,e),c) =
   match na with
-  | Name _ when force_wildcard () & noccurn (list_index na e) c ->
+  | Name _ when force_wildcard () & noccurn (List.index na e) c ->
       Anonymous
   | _ ->
       na
@@ -240,14 +240,14 @@ let rec build_tree na isgoal e ci cl =
   let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
   let cnl = ci.ci_cstr_ndecls in
   List.flatten
-    (list_tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
+    (List.tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
        (Array.length cl))
 
 and align_tree nal isgoal (e,c as rhs) = match nal with
   | [] -> [[],rhs]
   | na::nal ->
     match kind_of_term c with
-    | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e))
+    | Case (ci,p,c,cl) when c = mkRel (List.index na (snd e))
 	& (* don't contract if p dependent *)
 	computable p (ci.ci_pp_info.ind_nargs) ->
 	let clauses = build_tree na isgoal e ci cl in
@@ -579,7 +579,7 @@ let rec subst_cases_pattern subst pat =
   | PatVar _ -> pat
   | PatCstr (loc,((kn,i),j),cpl,n) ->
       let kn' = subst_ind subst kn
-      and cpl' = list_smartmap (subst_cases_pattern subst) cpl in
+      and cpl' = List.smartmap (subst_cases_pattern subst) cpl in
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
 
@@ -596,7 +596,7 @@ let rec subst_glob_constr subst raw =
 
   | GApp (loc,r,rl) ->
       let r' = subst_glob_constr subst r
-      and rl' = list_smartmap (subst_glob_constr subst) rl in
+      and rl' = List.smartmap (subst_glob_constr subst) rl in
 	if r' == r && rl' == rl then raw else
 	  GApp(loc,r',rl')
 
@@ -617,7 +617,7 @@ let rec subst_glob_constr subst raw =
 
   | GCases (loc,sty,rtno,rl,branches) ->
       let rtno' = Option.smartmap (subst_glob_constr subst) rtno
-      and rl' = list_smartmap (fun (a,x as y) ->
+      and rl' = List.smartmap (fun (a,x as y) ->
         let a' = subst_glob_constr subst a in
         let (n,topt) = x in
         let topt' = Option.smartmap
@@ -625,10 +625,10 @@ let rec subst_glob_constr subst raw =
             let sp' = subst_ind subst sp in
             if sp == sp' then t else (loc,(sp',i),y)) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
-      and branches' = list_smartmap
+      and branches' = List.smartmap
 			(fun (loc,idl,cpl,r as branch) ->
 			   let cpl' =
-			     list_smartmap (subst_cases_pattern subst) cpl
+			     List.smartmap (subst_cases_pattern subst) cpl
 			   and r' = subst_glob_constr subst r in
 			     if cpl' == cpl && r' == r then branch else
 			       (loc,idl,cpl',r'))
@@ -656,7 +656,7 @@ let rec subst_glob_constr subst raw =
       let ra1' = array_smartmap (subst_glob_constr subst) ra1
       and ra2' = array_smartmap (subst_glob_constr subst) ra2 in
       let bl' = array_smartmap
-        (list_smartmap (fun (na,k,obd,ty as dcl) ->
+        (List.smartmap (fun (na,k,obd,ty as dcl) ->
           let ty' = subst_glob_constr subst ty in
           let obd' = Option.smartmap (subst_glob_constr subst) obd in
           if ty'==ty & obd'==obd then dcl else (na,k,obd',ty')))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0740068721..9284e2c237 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -117,7 +117,7 @@ let check_conv_record (t1,sk1) (t2,sk2) =
 	| _ -> raise Not_found in
     let us2,extra_args2 =
       let l',s' = strip_app sk2_effective in
-      let bef,aft = list_chop (List.length us) l' in
+      let bef,aft = List.chop (List.length us) l' in
       (bef, append_stack_app_list aft s') in
     c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1,
     (n,zip(t2,sk2))
@@ -537,7 +537,7 @@ let evar_eqappr_x ts env evd pbty appr1 appr2 =
 (* We assume here |l1| <= |l2| *)
 
 let first_order_unification ts env evd (ev1,l1) (term2,l2) =
-  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+  let (deb2,rest2) = List.chop (List.length l2-List.length l1) l2 in
   ise_and evd
     (* First compare extra args for better failure message *)
     [(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
@@ -639,7 +639,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
         | Some _ -> error "Selection of specific occurrences not supported"
         | None ->
         let evty = set_holes evdref cty subst in
-        let instance = snd (list_filter2 (fun b c -> b) (filter,instance)) in
+        let instance = snd (List.filter2 (fun b c -> b) (filter,instance)) in
         let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
         evdref := evd;
         evsref := (fst (destEvar ev),evty)::!evsref;
@@ -761,7 +761,7 @@ let max_undefined_with_candidates evd =
         | Some l -> (evk,ev_info,l)::evars) evd [] in
   match l with
   | [] -> None
-  | a::l -> Some (list_last (a::l))
+  | a::l -> Some (List.last (a::l))
 
 let rec solve_unconstrained_evars_with_canditates evd =
   (* max_undefined is supposed to return the most recent, hence
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3256afd28b..0243a57801 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -172,7 +172,7 @@ let collect_evars emap c =
 	  else (* No recursion on the evar instantiation *) acc
       | _         ->
 	  fold_constr collrec acc c in
-  list_uniquize (collrec [] c)
+  List.uniquize (collrec [] c)
 
 let push_dependent_evars sigma emap =
   Evd.fold_undefined (fun ev {evar_concl = ccl} (sigma',emap') ->
@@ -242,7 +242,7 @@ let apply_subfilter filter subfilter =
          filter ([], List.rev subfilter))
 
 let extract_subfilter initial_filter refined_filter =
-  snd (list_filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
+  snd (List.filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
 
 (**********************)
 (* Creating new evars *)
@@ -320,7 +320,7 @@ let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
 
 let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
   assert (not !Flags.debug ||
-            list_distinct (ids_of_named_context (named_context_of_val sign)));
+            List.distinct (ids_of_named_context (named_context_of_val sign)));
   let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
   (evd,mkEvar (newevk,Array.of_list instance))
 
@@ -333,7 +333,7 @@ let new_evar evd env ?src ?filter ?candidates typ =
   let instance =
     match filter with
     | None -> instance
-    | Some filter -> list_filter_with filter instance in
+    | Some filter -> List.filter_with filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates instance
 
 let new_type_evar ?src ?filter evd env =
@@ -369,7 +369,7 @@ let restrict_evar_key evd evk filter candidates =
     let sign = evar_hyps evi in
     let src = evi.evar_source in
     let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
-    let ctxt = snd (list_filter2 (fun b c -> b) (filter,evar_context evi)) in
+    let ctxt = snd (List.filter2 (fun b c -> b) (filter,evar_context evi)) in
     let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
     Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
 
@@ -501,7 +501,7 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) =
 let expand_alias_once aliases x =
   match get_alias_chain_of aliases x with
   | []  -> None
-  | l -> Some (list_last l)
+  | l -> Some (List.last l)
 
 let expansions_of_var aliases x =
   match get_alias_chain_of aliases x with
@@ -744,7 +744,7 @@ let is_unification_pattern_evar env evd (evk,args) l t =
     let args = remove_instance_local_defs evd evk (Array.to_list args) in
     let n = List.length args in
     match find_unification_pattern_args env (args @ l) t with
-    | Some l -> Some (list_skipn n l)
+    | Some l -> Some (List.skipn n l)
     | _ -> None
   else
     None
@@ -854,7 +854,7 @@ let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
   let ids = List.map pi1 (named_context_of_val sign) in
-  let inst_in_sign = List.map mkVar (list_filter_with filter ids) in
+  let inst_in_sign = List.map mkVar (List.filter_with filter ids) in
   let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
   (evd,whd_evar evd evar_in_sign)
 
@@ -881,7 +881,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let sign1 = evar_hyps evi1 in
   let filter1 = evar_filter evi1 in
   let ids1 = List.map pi1 (named_context_of_val sign1) in
-  let inst_in_sign = List.map mkVar (list_filter_with filter1 ids1) in
+  let inst_in_sign = List.map mkVar (List.filter_with filter1 ids1) in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
     List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
       let id = next_name_away na avoid in
@@ -1179,9 +1179,9 @@ let filter_candidates evd evk filter candidates =
   match candidates,filter with
   | None,_ | _, None -> candidates
   | Some l, Some filter ->
-      let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
+      let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
       Some (List.filter (fun a ->
-        list_subset (Idset.elements (collect_vars a)) ids) l)
+        List.subset (Idset.elements (collect_vars a)) ids) l)
 
 let closure_of_filter evd evk filter =
   let evi = Evd.find_undefined evd evk in
@@ -1407,7 +1407,7 @@ let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 a
   if are_canonical_instances args1 args2 env then
     (* If instances are canonical, we solve the problem in linear time *)
     let sign = evar_filtered_context (Evd.find evd evk2) in
-    let id_inst = list_map_to_array (fun (id,_,_) -> mkVar id) sign in
+    let id_inst = List.map_to_array (fun (id,_,_) -> mkVar id) sign in
     Evd.define evk2 (mkEvar(evk1,id_inst)) evd
   else
     let evd,ev1,ev2 =
@@ -1476,7 +1476,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
   | None -> raise NoCandidates
   | Some l ->
       let l' =
-        list_map_filter
+        List.map_filter
           (filter_compatible_candidates conv_algo env evd evi args rhs) l in
       match l' with
       | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a73a74f457..7d95e743d0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -56,7 +56,7 @@ let evar_body evi = evi.evar_body
 let evar_filter evi = evi.evar_filter
 let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
 let evar_filtered_context evi =
-  snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
+  snd (List.filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
 let evar_env evi =
   List.fold_right push_named (evar_filtered_context evi)
     (reset_context (Global.env()))
@@ -676,7 +676,7 @@ let rec list_assoc_in_triple x = function
 
 let subst_defined_metas bl c =
   let rec substrec c = match kind_of_term c with
-    | Meta i -> substrec (list_assoc_snd_in_triple i bl)
+    | Meta i -> substrec (List.assoc_snd_in_triple i bl)
     | _ -> map_constr substrec c
   in try Some (substrec c) with Not_found -> None
 
@@ -797,9 +797,9 @@ let evar_dependency_closure n sigma =
     if n=0 then l
     else
       let l' =
-        list_map_append (fun (evk,_) ->
+        List.map_append (fun (evk,_) ->
           try ExistentialMap.find evk graph with Not_found -> []) l in
-      aux (n-1) (list_uniquize (Sort.list order (l@l'))) in
+      aux (n-1) (List.uniquize (Sort.list order (l@l'))) in
   aux n (undefined_list sigma)
 
 let pr_evar_map_t depth sigma =
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index a090094aaa..d20afaf403 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -36,7 +36,7 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
 let map_glob_constr_left_to_right f = function
   | GApp (loc,g,args) ->
       let comp1 = f g in
-      let comp2 = Util.list_map_left f args in
+      let comp2 = Util.List.map_left f args in
       GApp (loc,comp1,comp2)
   | GLambda (loc,na,bk,ty,c) ->
       let comp1 = f ty in
@@ -52,8 +52,8 @@ let map_glob_constr_left_to_right f = function
       GLetIn (loc,na,comp1,comp2)
   | GCases (loc,sty,rtntypopt,tml,pl) ->
       let comp1 = Option.map f rtntypopt in
-      let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in
-      let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
+      let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
+      let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
       GCases (loc,sty,comp1,comp2,comp3)
   | GLetTuple (loc,nal,(na,po),b,c) ->
       let comp1 = Option.map f po in
@@ -66,7 +66,7 @@ let map_glob_constr_left_to_right f = function
       let comp3 = f b2 in
       GIf (loc,f c,(na,comp1),comp2,comp3)
   | GRec (loc,fk,idl,bl,tyl,bv) ->
-      let comp1 = Array.map (Util.list_map_left (map_glob_decl_left_to_right f)) bl in
+      let comp1 = Array.map (Util.List.map_left (map_glob_decl_left_to_right f)) bl in
       let comp2 = Array.map f tyl in
       let comp3 = Array.map f bv in
       GRec (loc,fk,idl,comp1,comp2,comp3)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 025f7f6687..f11fb46134 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -134,7 +134,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
      	| Ind (_,_) ->
-	    let realargs = list_skipn nparams largs in
+	    let realargs = List.skipn nparams largs in
 	    let base = applist (lift i pk,realargs) in
             if depK then
 	      Reduction.beta_appvect
@@ -209,7 +209,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
-            let realargs = list_skipn nparrec largs
+            let realargs = List.skipn nparrec largs
             and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
@@ -431,7 +431,7 @@ let mis_make_indrec env sigma listdepkind mib =
 	mis_make_case_com dep env sigma indi (mibi,mipi) kind
   in
     (* Body of mis_make_indrec *)
-    list_tabulate make_one_rec nrec
+    List.tabulate make_one_rec nrec
 
 (**********************************************************************)
 (* This builds elimination predicate for Case tactic *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 19126f01bc..a026f53d4e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -91,7 +91,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkInd ((fst ind),ntypes-k-1) in
   if j > nconstr then error "Not enough constructors in the type.";
-  substl (list_tabulate make_Ik ntypes) specif.(j-1)
+  substl (List.tabulate make_Ik ntypes) specif.(j-1)
 
 (* Arity of constructors excluding parameters and local defs *)
 
@@ -219,7 +219,7 @@ let get_constructor (ind,mib,mip,params) j =
   let typi = instantiate_params typi params mib.mind_params_ctxt in
   let (args,ccl) = decompose_prod_assum typi in
   let (_,allargs) = decompose_app ccl in
-  let vargs = list_skipn (List.length params) allargs in
+  let vargs = List.skipn (List.length params) allargs in
   { cs_cstr = ith_constructor_of_inductive ind j;
     cs_params = params;
     cs_nargs = rel_context_length args;
@@ -258,11 +258,11 @@ let get_arity env (ind,params) =
     let parsign = mib.mind_params_ctxt in
     let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
     if List.length params = rel_context_nhyps parsign - nnonrecparams then
-      snd (list_chop nnonrecparams mib.mind_params_ctxt)
+      snd (List.chop nnonrecparams mib.mind_params_ctxt)
     else
       parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
-  let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in
+  let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
   let subst = instantiate_context parsign params in
   (substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
 
@@ -324,7 +324,7 @@ let find_rectype env sigma c =
   match kind_of_term t with
     | Ind ind ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
-        let (par,rargs) = list_chop mib.mind_nparams l in
+        let (par,rargs) = List.chop mib.mind_nparams l in
         IndType((ind, par),rargs)
     | _ -> raise Not_found
 
@@ -406,7 +406,7 @@ let type_case_branches_with_names env indspec p c =
   let (ind,args) = indspec in
   let (mib,mip as specif) = Inductive.lookup_mind_specif env ind in
   let nparams = mib.mind_nparams in
-  let (params,realargs) = list_chop nparams args in
+  let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
   (* Build case type *)
   let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index bc9c832ae7..37cbcc0629 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -110,7 +110,7 @@ let dummy_constr = mkProp
 let rec make_renaming ids = function
   | (Name id,Name _,_)::stk ->
       let renaming = make_renaming ids stk in
-      (try mkRel (list_index id ids) :: renaming
+      (try mkRel (List.index id ids) :: renaming
        with Not_found -> dummy_constr :: renaming)
   | (_,_,_)::stk ->
       dummy_constr :: make_renaming ids stk
@@ -152,7 +152,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 		 | _ -> error "Only bound indices allowed in second order pattern matching.")
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
-	  if list_subset frels relargs then
+	  if List.subset frels relargs then
 	    constrain (n,([],build_lambda relargs stk cT)) subst
 	  else
 	    raise PatternMatchingFailure
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c3b03e209d..e4ae1e4b85 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -146,13 +146,13 @@ let instantiate_pattern sigma lvar c =
 	let ctx,c = List.assoc id lvar in
 	try
 	  let inst =
-	    List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in
+	    List.map (fun id -> mkRel (List.index (Name id) vars)) ctx in
 	  let c = substl inst c in
 	  snd (pattern_of_constr sigma c)
-	with Not_found (* list_index failed *) ->
+	with Not_found (* List.index failed *) ->
 	  let vars =
-	    list_map_filter (function Name id -> Some id | _ -> None) vars in
-	  error_instantiate_pattern id (list_subtract ctx vars)
+	    List.map_filter (function Name id -> Some id | _ -> None) vars in
+	  error_instantiate_pattern id (List.subtract ctx vars)
        with Not_found (* List.assoc failed *) ->
 	 x)
   | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
@@ -183,7 +183,7 @@ let rec subst_pattern subst pat =
 	if f' == f && args' == args then pat else
 	  PApp (f',args')
   | PSoApp (i,args) ->
-      let args' = list_smartmap (subst_pattern subst) args in
+      let args' = List.smartmap (subst_pattern subst) args in
 	if args' == args then pat else
 	  PSoApp (i,args')
   | PLambda (name,c1,c2) ->
@@ -219,7 +219,7 @@ let rec subst_pattern subst pat =
 	let c' = subst_pattern subst c in
 	if c' == c then br else (i,n,c')
       in
-      let branches' = list_smartmap subst_branch branches in
+      let branches' = List.smartmap subst_branch branches in
       if cip' == cip && typ' == typ && c' == c && branches' == branches
       then pat
       else PCase(cip', typ', c', branches')
@@ -241,7 +241,7 @@ let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
 
 let rec pat_of_raw metas vars = function
   | GVar (_,id) ->
-      (try PRel (list_index (Name id) vars)
+      (try PRel (List.index (Name id) vars)
        with Not_found -> PVar id)
   | GPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5113236954..0eff92b617 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -79,7 +79,7 @@ let search_guard loc env possible_indexes fixdefs =
 	    let fix = ((indexes, 0),fixdefs) in
 	    try check_fix env fix; raise (Found indexes)
 	    with TypeError _ -> ())
-	 (list_combinations possible_indexes);
+	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
        if loc = Loc.ghost then error errmsg else
 	 user_err_loc (loc,"search_guard", Pp.str errmsg)
@@ -363,7 +363,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 		Array.to_list (Array.mapi
 				 (fun i (n,_) -> match n with
 				  | Some n -> [n]
-				  | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
+				  | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i))
 				 vn)
 	      in
 	      let fixdecls = (names,ftys,fdefs) in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7c128d245d..96b57ae183 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -65,7 +65,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
   let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
-   list_smartmap
+   List.smartmap
      (Option.smartmap (fun kn -> fst (subst_con subst kn)))
     projs
   in
@@ -227,7 +227,7 @@ let compute_canonical_projections (con,ind) =
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
-  let params, projs = list_chop p args in
+  let params, projs = List.chop p args in
   let lpj = keep_true_projections lpj kl in
   let lps = List.combine lpj projs in
   let comp =
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index e10a64dc53..46f6684765 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -18,13 +18,13 @@ let make_red_flag l =
 	if red.rDelta then
 	  Errors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
-        add_flag { red with rConst = Util.list_union red.rConst l } lf
+        add_flag { red with rConst = Util.List.union red.rConst l } lf
     | FDeltaBut l :: lf ->
 	if red.rConst <> [] & not red.rDelta then
 	  Errors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
         add_flag
-	  { red with rConst = Util.list_union red.rConst l; rDelta = true }
+	  { red with rConst = Util.List.union red.rConst l; rDelta = true }
 	  lf
   in
   add_flag
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0b5ad7b0bf..fd9a312fc4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -58,7 +58,7 @@ let rec strip_app = function
 let strip_n_app n s =
   let apps,s' = strip_app s in
   try
-    let bef,aft = list_chop n apps in
+    let bef,aft = List.chop n apps in
     match aft with
       |h::[] -> Some (bef,h,s')
       |h::t -> Some (bef,h,append_stack_app_list t s')
@@ -66,7 +66,7 @@ let strip_n_app n s =
   with
     |Failure _ -> None
 let nfirsts_app_of_stack n s =
-  let (args, _) = strip_app s in list_firstn n args
+  let (args, _) = strip_app s in List.firstn n args
 let list_of_app_stack s =
   let (out,s') = strip_app s in
   Option.init (s' = []) out
@@ -88,7 +88,7 @@ let rec stack_assign s p c = match s with
       if p >= q then
 	Zapp args :: stack_assign s (p-q) c
       else
-        (match list_chop p args with
+        (match List.chop p args with
             (bef, _::aft) -> Zapp (bef@c::aft) :: s
           | _ -> assert false)
   | _ -> s
@@ -98,7 +98,7 @@ let rec stack_tail p s =
       | Zapp args :: s ->
 	  let q = List.length args in
 	  if p >= q then stack_tail (p-q) s
-	  else Zapp (list_skipn p args) :: s
+	  else Zapp (List.skipn p args) :: s
       | _ -> failwith "stack_tail"
 let rec stack_nth s p = match s with
   | Zapp args :: s ->
@@ -241,13 +241,13 @@ let reducible_mind_case c = match kind_of_term c with
 let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
-  substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
+  substl (List.tabulate make_Fi nbodies) bodies.(bodynum)
 
 let reduce_mind_case mia =
   match kind_of_term mia.mconstr with
     | Construct (ind_sp,i) ->
 (*	let ncargs = (fst mia.mci).(i-1) in*)
-	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
+	let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
         applist (mia.mlf.(i-1),real_cargs)
     | CoFix cofix ->
 	let cofix_def = contract_cofix cofix in
@@ -260,7 +260,7 @@ let reduce_mind_case mia =
 let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
   let nbodies = Array.length recindices in
   let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
-  substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
+  substl (List.tabulate make_Fi nbodies) bodies.(bodynum)
 
 let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum & bodynum < Array.length recindices);
@@ -338,7 +338,7 @@ let rec whd_state_gen flags ts env sigma =
 	if red_iota flags then
 	  match strip_app stack with
 	  |args, (Zcase(ci, _, lf)::s') ->
-	    whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
 	  |args, (Zfix (f,s')::s'') ->
 	    let x' = applist(x,args) in
 	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
@@ -404,7 +404,7 @@ let local_whd_state_gen flags sigma =
 	if red_iota flags then
 	  match strip_app stack with
 	  |args, (Zcase(ci, _, lf)::s') ->
-	    whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
 	  |args, (Zfix (f,s')::s'') ->
 	    let x' = applist(x,args) in
 	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
@@ -590,7 +590,7 @@ let whd_betaiota_preserving_vm_cast env sigma t =
        | Construct (ind,c) -> begin
 	 match strip_app stack with
 	   |args, (Zcase(ci, _, lf)::s') ->
-	     whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+	     whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
 	   |args, (Zfix (f,s')::s'') ->
 	     let x' = applist(x,args) in
 	     whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
@@ -888,7 +888,7 @@ let whd_programs_stack env sigma =
       | Construct (ind,c) -> begin
 	match strip_app stack with
 	  |args, (Zcase(ci, _, lf)::s') ->
-	    whrec (lf.(c-1), append_stack_app_list (list_skipn ci.ci_npar args) s')
+	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
 	  |args, (Zfix (f,s')::s'') ->
 	    let x' = applist(x,args) in
 	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9791598fd8..b897c01afb 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -186,12 +186,12 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
 	     raise Elimconst) args
   in
   let reversible_rels = List.map fst li in
-  if not (list_distinct reversible_rels) then
+  if not (List.distinct reversible_rels) then
     raise Elimconst;
-  list_iter_i (fun i t_i ->
+  List.iter_i (fun i t_i ->
     if not (List.mem_assoc (i+1) li) then
       let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
-      if list_intersect fvs reversible_rels <> [] then raise Elimconst)
+      if List.intersect fvs reversible_rels <> [] then raise Elimconst)
     labs;
   let k = lv.(i) in
   if k < nargs then
@@ -322,13 +322,13 @@ let reference_eval sigma env = function
 let x = Name (id_of_string "x")
 
 let make_elim_fun (names,(nbfix,lv,n)) largs =
-  let lu = list_firstn n largs in
+  let lu = List.firstn n largs in
   let p = List.length lv in
   let lyi = List.map fst lv in
   let la =
-    list_map_i (fun q aq ->
+    List.map_i (fun q aq ->
       (* k from the comment is q+1 *)
-      try mkRel (p+1-(list_index (n-q) lyi))
+      try mkRel (p+1-(List.index (n-q) lyi))
       with Not_found -> aq)
       0 (List.map (lift p) lu)
   in
@@ -338,8 +338,8 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
       | Some (minargs,ref) ->
           let body = applistc (mkEvalRef ref) la in
           let g =
-            list_fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
-              let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
+            List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
+              let subst = List.map (lift (-q)) (List.firstn (n-ij) la) in
               let tij' = substl (List.rev subst) tij in
 	      mkLambda (x,tij',c)) 1 body (List.rev lv)
           in Some (minargs,g)
@@ -433,7 +433,7 @@ let reduce_fix whdfun sigma fix stack =
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') = whdfun sigma recarg in
-        let stack' = list_assign stack recargnum (applist recarg') in
+        let stack' = List.assign stack recargnum (applist recarg') in
 	(match kind_of_term recarg'hd with
            | Construct _ -> Reduced (contract_fix fix, stack')
 	   | _ -> NotReducible)
@@ -442,7 +442,7 @@ let contract_fix_use_function env sigma f
   ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
-  let lbodies = list_tabulate make_Fi nbodies in
+  let lbodies = List.tabulate make_Fi nbodies in
   substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
@@ -455,7 +455,7 @@ let reduce_fix_use_function env sigma f whfun fix stack =
 	    (recarg, [])
 	  else
 	    whfun recarg in
-        let stack' = list_assign stack recargnum (applist recarg') in
+        let stack' = List.assign stack recargnum (applist recarg') in
 	(match kind_of_term recarg'hd with
            | Construct _ ->
 	       Reduced (contract_fix_use_function env sigma f fix,stack')
@@ -465,14 +465,14 @@ let contract_cofix_use_function env sigma f
   (bodynum,(_names,_,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
-  let subbodies = list_tabulate make_Fi nbodies in
+  let subbodies = List.tabulate make_Fi nbodies in
   substl_checking_arity env (List.rev subbodies)
     (nf_beta sigma bodies.(bodynum))
 
 let reduce_mind_case_use_function func env sigma mia =
   match kind_of_term mia.mconstr with
     | Construct(ind_sp,i) ->
-	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
+	let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
 	applist (mia.mlf.(i-1), real_cargs)
     | CoFix (bodynum,(names,_,_) as cofix) ->
 	let build_cofix_name =
@@ -661,7 +661,7 @@ let rec red_elim_const env sigma ref largs =
           let arg = List.nth stack i in
           let rarg = whd_construct_stack env sigma arg in
           match kind_of_term (fst rarg) with
-          | Construct _ -> list_assign stack i (applist rarg)
+          | Construct _ -> List.assign stack i (applist rarg)
           | _ -> raise Redelimination)
         largs l, n >= 0 && l =  [] && nargs >= n,
                  n >= 0 && l <> [] && nargs >= n in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index e4f481e58d..765f1e4fa7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -286,10 +286,10 @@ let adjust_app_list_size f1 l1 f2 l2 =
   let len1 = List.length l1 and len2 = List.length l2 in
   if len1 = len2 then (f1,l1,f2,l2)
   else if len1 < len2 then
-   let extras,restl2 = list_chop (len2-len1) l2 in
+   let extras,restl2 = List.chop (len2-len1) l2 in
     (f1, l1, applist (f2,extras), restl2)
   else
-    let extras,restl1 = list_chop (len1-len2) l1 in
+    let extras,restl1 = List.chop (len1-len2) l1 in
     (applist (f1,extras), restl1, f2, l2)
 
 let adjust_app_array_size f1 l1 f2 l2 =
@@ -550,7 +550,7 @@ let free_rels m =
 let collect_metas c =
   let rec collrec acc c =
     match kind_of_term c with
-      | Meta mv -> list_add_set mv acc
+      | Meta mv -> List.add_set mv acc
       | _       -> fold_constr collrec acc c
   in
   List.rev (collrec [] c)
@@ -691,7 +691,7 @@ let replace_term = replace_term_gen eq_constr
    except the ones in l *)
 
 let error_invalid_occurrence l =
-  let l = list_uniquize (List.sort Pervasives.compare l) in
+  let l = List.uniquize (List.sort Pervasives.compare l) in
   errorlabstrm ""
     (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
      prlist_with_sep spc int l ++ str ".")
@@ -951,7 +951,7 @@ let align_prod_letin c a : rel_context * constr =
   let (lc,_,_) = decompose_prod_letin c in
   let (la,l,a) = decompose_prod_letin a in
   if not (la >= lc) then invalid_arg "align_prod_letin";
-  let (l1,l2) = Util.list_chop lc l in
+  let (l1,l2) = Util.List.chop lc l in
   l2,it_mkProd_or_LetIn a l1
 
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
@@ -1045,7 +1045,7 @@ let adjust_subst_to_rel_context sign l =
     | _ -> anomaly "Instance and signature do not match"
   in aux [] (List.rev sign) l
 
-let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
+let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let rec mem_named_context id = function
   | (id',_,_) :: _ when id=id' -> true
@@ -1098,7 +1098,7 @@ let context_chop k ctx =
 (* Do not skip let-in's *)
 let env_rel_context_chop k env =
   let rels = rel_context env in
-  let ctx1,ctx2 = list_chop k rels in
+  let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
   ctx1
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 8fd0f768ea..426197af29 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -154,13 +154,13 @@ let subst_class (subst,cl) =
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
-  let do_subst_ctx ctx = list_smartmap
+  let do_subst_ctx ctx = List.smartmap
     (fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t))
     ctx in
   let do_subst_context (grs,ctx) =
-    list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+    List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
     do_subst_ctx ctx in
-  let do_subst_projs projs = list_smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in
+  let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in
   { cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
@@ -195,7 +195,7 @@ let discharge_class (_,cl) =
 	| Some (_, (tc, _)) -> Some (tc.cl_impl, true))
 	ctx' 
       in
-	list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+	List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
 	  @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
@@ -207,7 +207,7 @@ let discharge_class (_,cl) =
     { cl_impl = cl_impl';
       cl_context = context;
       cl_props = props;
-      cl_projs = list_smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
+      cl_projs = List.smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
 
 let rebuild_class cl = 
   try 
@@ -246,7 +246,7 @@ let build_subclasses ~check env sigma glob pri =
       | Some (rels, (tc, args)) ->
 	let instapp = Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) in
 	let projargs = Array.of_list (args @ [instapp]) in
-	let projs = list_map_filter 
+	let projs = List.map_filter 
 	  (fun (n, b, proj) ->
 	   match b with 
 	   | None -> None
@@ -408,12 +408,12 @@ let add_inductive_class ind =
 
 let instance_constructor cl args =
   let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
-  let pars = fst (list_chop lenpars args) in
+  let pars = fst (List.chop lenpars args) in
     match cl.cl_impl with
       | IndRef ind -> Some (applistc (mkConstruct (ind, 1)) args),
 	  applistc (mkInd ind) pars
       | ConstRef cst -> 
-	let term = if args = [] then None else Some (list_last args) in
+	let term = if args = [] then None else Some (List.last args) in
 	  term, applistc (mkConst cst) pars
       | _ -> assert false
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index df1833f843..b24992b8d7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -100,7 +100,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
 let e_type_case_branches env evdref (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 = e_is_correct_arity env evdref c pj ind specif params in
   let lc = build_branches_type ind specif params p in