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

9 files changed, 81 insertions, 81 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3ccfe21d87..c54dc81202 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -229,12 +229,12 @@ let minductive_message = function
 
 let check_all_names_different indl =
   let ind_names = List.map (fun ind -> ind.ind_name) indl in
-  let cstr_names = list_map_append (fun ind -> List.map fst ind.ind_lc) indl in
-  let l = list_duplicates ind_names in
+  let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
+  let l = List.duplicates ind_names in
   if l <> [] then raise (InductiveError (SameNamesTypes (List.hd l)));
-  let l = list_duplicates cstr_names in
+  let l = List.duplicates cstr_names in
   if l <> [] then raise (InductiveError (SameNamesConstructors (List.hd l)));
-  let l = list_intersect ind_names cstr_names in
+  let l = List.intersect ind_names cstr_names in
   if l <> [] then raise (InductiveError (SameNamesOverlap l))
 
 let mk_mltype_data evdref env assums arity indname =
@@ -286,7 +286,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
      (* Temporary declaration of notations and scopes *)
      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
      (* Interpret the constructor types *)
-     list_map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl)
+     List.map3 (interp_cstrs evdref env_ar_params impls) mldatas arities indl)
      () in
 
   (* Instantiate evars and check all are resolved *)
@@ -303,7 +303,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
     constructors;
 
   (* Build the inductive entries *)
-  let entries = list_map3 (fun ind arity (cnames,ctypes,cimpls) -> {
+  let entries = List.map3 (fun ind arity (cnames,ctypes,cimpls) -> {
     mind_entry_typename = ind.ind_name;
     mind_entry_arity = arity;
     mind_entry_consnames = cnames;
@@ -368,11 +368,11 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let (_,kn) = declare_mind isrecord mie in
   let mind = Global.mind_of_delta_kn kn in
-  list_iter_i (fun i (indimpls, constrimpls) ->
+  List.iter_i (fun i (indimpls, constrimpls) ->
 		   let ind = (mind,i) in
 		     Autoinstance.search_declaration (IndRef ind);
 		     maybe_declare_manual_implicits false (IndRef ind) indimpls;
-		     list_iter_i
+		     List.iter_i
 		       (fun j impls ->
 (*	    Autoinstance.search_declaration (ConstructRef (ind,j));*)
 			  maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
@@ -423,7 +423,7 @@ let rec partial_order = function
     let rec browse res xge' = function
     | [] ->
 	let res = List.map (function
-	  | (z, Inr zge) when List.mem x zge -> (z, Inr (list_union zge xge'))
+	  | (z, Inr zge) when List.mem x zge -> (z, Inr (List.union zge xge'))
 	  | r -> r) res in
 	(x,Inr xge')::res
     | y::xge ->
@@ -438,13 +438,13 @@ let rec partial_order = function
 		  if t = y then (z, Inl x) else (z, Inl t)
 	      | (z, Inr zge) ->
 		  if List.mem y zge then
-		    (z, Inr (list_add_set x (list_remove y zge)))
+		    (z, Inr (List.add_set x (List.remove y zge)))
 		  else
 		    (z, Inr zge)) res in
-	    browse ((y,Inl x)::res) xge' (list_union xge (list_remove x yge))
+	    browse ((y,Inl x)::res) xge' (List.union xge (List.remove x yge))
 	  else
-	    browse res (list_add_set y (list_union xge' yge)) xge
-	with Not_found -> browse res (list_add_set y xge') xge
+	    browse res (List.add_set y (List.union xge' yge)) xge
+	with Not_found -> browse res (List.add_set y xge') xge
       in link y
     in browse (partial_order rest) [] xge
 
@@ -734,12 +734,12 @@ let interp_recursive isfix fixl notations =
   (* Interp arities allowing for unresolved types *)
   let evdref = ref Evd.empty in
   let fixctxs, fiximppairs, fixannots =
-    list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in
+    List.split3 (List.map (interp_fix_context evdref env isfix) fixl) in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
-  let fixccls,fixcclimps = List.split (list_map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
+  let fixccls,fixcclimps = List.split (List.map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
-  let fiximps = list_map3
+  let fiximps = List.map3
     (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
     fixctximps fixcclimps fixctxs in
   let rec_sign =
@@ -764,7 +764,7 @@ let interp_recursive isfix fixl notations =
   let fixdefs =
     Metasyntax.with_syntax_protection (fun () ->
       List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
-      list_map4
+      List.map4
 	(fun fixctximpenv -> interp_fix_body evdref env_rec (Idmap.fold Idmap.add fixctximpenv impls))
 	fixctximpenvs fixctxs fixl fixccls)
       () in
@@ -776,7 +776,7 @@ let interp_recursive isfix fixl notations =
   let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
+  (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
 
 let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) =
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
@@ -795,7 +795,7 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -808,8 +808,8 @@ let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     let indexes = search_guard Loc.ghost (Global.env()) indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let fixdecls =
-      list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    ignore (list_map4 (declare_fix Fixpoint) fixnames fixdecls fixtypes fiximps);
+      List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+    ignore (List.map4 (declare_fix Fixpoint) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
   end;
@@ -820,7 +820,7 @@ let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -830,9 +830,9 @@ let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns =
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
-    let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+    let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    ignore (list_map4 (declare_fix CoFixpoint) fixnames fixdecls fixtypes fiximps);
+    ignore (List.map4 (declare_fix CoFixpoint) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
   end;
@@ -911,7 +911,7 @@ let do_program_recursive fixkind fixl ntns =
   let (fixnames,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
   let fixdefs = List.map Option.get fixdefs in
-  let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
+  let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
     if isfix then begin
       let possible_indexes = List.map compute_possible_guardness_evidences info in
       let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
@@ -920,7 +920,7 @@ let do_program_recursive fixkind fixl ntns =
       in
       let indexes = 
 	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
-	list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
+	List.iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
     end;
     Obligations.add_mutual_definitions defs ntns fixkind
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 5ed45535ad..92b0d65365 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -38,7 +38,7 @@ let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in
   let nhyp = named_context_length hyps in
   let args = instance_from_named_context (List.rev hyps) in
-  let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
+  let subs = List.tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
   let inds' =
     List.map
       (function (tname,arity,cnames,lc) ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3cdeb0be90..53c4325e10 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1014,7 +1014,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
 	   let filter =
 	     function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
-	   let unboundvars = list_map_filter filter unboundvars in
+	   let unboundvars = List.map_filter filter unboundvars in
 	   quote (pr_glob_constr_env (Global.env()) c) ++
 	     (if unboundvars <> [] or vars <> [] then
 		strbrk " (with " ++
@@ -1027,7 +1027,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
        else if n>2 then str " (repeated "++int n++str" times)"
        else mt()) in
     if calls <> [] then
-      let kind_of_last_call = match list_last calls with
+      let kind_of_last_call = match List.last calls with
     | (_,Proof_type.LtacConstrInterp _) -> ", last term evaluation failed."
     | _ -> ", last call failed." in
     hov 0 (str "In nested Ltac calls to " ++
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index b99f83e5cd..b3ea8438ac 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -176,7 +176,7 @@ let beq_scheme_msg mind =
   (* TODO: mutual inductive case *)
   str "Boolean equality on " ++
     pr_enum (fun ind -> quote (Printer.pr_inductive (Global.env()) ind))
-    (list_tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
+    (List.tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
 
 let declare_beq_scheme_with l kn =
   try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
@@ -219,7 +219,7 @@ let declare_one_induction_scheme ind =
   let from_prop = kind = InProp in
   let kelim = elim_sorts (mib,mip) in
   let elims =
-    list_map_filter (fun (sort,kind) ->
+    List.map_filter (fun (sort,kind) ->
       if List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop else kinds_from_type) in
   List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind))
@@ -365,10 +365,10 @@ let get_common_underlying_mutual_inductive = function
       | (_,ind')::_ ->
 	  raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
       | [] ->
-	  if not (list_distinct (List.map snd (List.map snd all))) then
+	  if not (List.distinct (List.map snd (List.map snd all))) then
 	    error "A type occurs twice";
 	  mind,
-	  list_map_filter
+	  List.map_filter
 	    (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
 
 let do_scheme l =
@@ -394,7 +394,7 @@ let list_split_rev_at index l =
   let rec aux i acc = function
       hd :: tl when i = index -> acc, tl
     | hd :: tl -> aux (succ i) (hd :: acc) tl
-    | [] -> failwith "list_split_when: Invalid argument"
+    | [] -> failwith "List.split_when: Invalid argument"
   in aux 0 [] l
 
 let fold_left' f = function
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 0c9cf877d0..25a8e9208a 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -84,7 +84,7 @@ let find_mutually_recursive_statements thms =
         (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
         (Global.env()) hyps in
       let ind_hyps =
-        List.flatten (list_map_i (fun i (_,b,t) ->
+        List.flatten (List.map_i (fun i (_,b,t) ->
           match kind_of_term t with
           | Ind (kn,_ as ind) when
                 let mind = Global.lookup_mind kn in
@@ -108,14 +108,14 @@ let find_mutually_recursive_statements thms =
     (* Check if all conclusions are coinductive in the same type *)
     (* (degenerated cartesian product since there is at most one coind ccl) *)
     let same_indccl =
-      list_cartesians_filter (fun hyp oks ->
+      List.cartesians_filter (fun hyp oks ->
 	if List.for_all (of_same_mutind hyp) oks
 	then Some (hyp::oks) else None) [] ind_ccls in
     let ordered_same_indccl =
-      List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
+      List.filter (List.for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
     (* Check if some hypotheses are inductive in the same type *)
     let common_same_indhyp =
-      list_cartesians_filter (fun hyp oks ->
+      List.cartesians_filter (fun hyp oks ->
 	if List.for_all (of_same_mutind hyp) oks
 	then Some (hyp::oks) else None) [] inds_hyps in
     let ordered_inds,finite,guard =
@@ -129,11 +129,11 @@ let find_mutually_recursive_statements thms =
           indccl, true, []
       | [], _::_ ->
 	  if same_indccl <> [] &&
-	     list_distinct (List.map pi1 (List.hd same_indccl)) then
+	     List.distinct (List.map pi1 (List.hd same_indccl)) then
 	    if_verbose msg_info (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all ();
           let possible_guards = List.map (List.map pi3) inds_hyps in
 	  (* assume the largest indices as possible *)
-	  list_last common_same_indhyp, false, possible_guards
+	  List.last common_same_indhyp, false, possible_guards
       | _, [] ->
 	  error
             ("Cannot find common (mutual) inductive premises or coinductive" ^
@@ -265,7 +265,7 @@ let rec_tac_initializer finite guard thms snl =
   else
     (* nl is dummy: it will be recomputed at Qed-time *)
     let nl = match snl with 
-     | None -> List.map succ (List.map list_last guard)
+     | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
     in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
        | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
@@ -302,7 +302,7 @@ let start_proof_with_initialization kind recguard thms snl hook =
           if other_thms = [] then [] else
             (* there are several theorems defined mutually *)
             let body,opaq = retrieve_first_recthm ref in
-            list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
+            List.map_i (save_remaining_recthms kind body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4eebfc8f73..534a0a7dd4 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -372,7 +372,7 @@ let analyze_notation_tokens l =
   let l = raw_analyze_notation_tokens l in
   let vars = get_notation_vars l in
   let recvars,l = interp_list_parser [] l in
-  recvars, list_subtract vars (List.map snd recvars), l
+  recvars, List.subtract vars (List.map snd recvars), l
 
 let error_not_same_scope x y =
   error ("Variables "^string_of_id x^" and "^string_of_id y^
@@ -448,7 +448,7 @@ let make_hunks etyps symbols from =
   let vars,typs = List.split etyps in
   let rec make ws = function
     | NonTerminal m :: prods ->
-	let i = list_index m vars in
+	let i = List.index m vars in
 	let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
 	let u = UnpMetaVar (i,prec) in
 	if prods <> [] && is_non_terminal (List.hd prods) then
@@ -494,14 +494,14 @@ let make_hunks etyps symbols from =
 	add_break n (make NoBreak prods)
 
     | SProdList (m,sl) :: prods ->
-	let i = list_index m vars in
+	let i = List.index m vars in
 	let typ = List.nth typs (i-1) in
 	let _,prec = precedence_of_entry_type from typ in
         let sl' =
           (* If no separator: add a break *)
 	  if sl = [] then add_break 1 []
           (* We add NonTerminal for simulation but remove it afterwards *)
-	  else snd (list_sep_last (make NoBreak (sl@[NonTerminal m]))) in
+	  else snd (List.sep_last (make NoBreak (sl@[NonTerminal m]))) in
 	let hunk = match typ with
 	  | ETConstr _ -> UnpListMetaVar (i,prec,sl')
 	  | ETBinder isopen ->
@@ -560,7 +560,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
       when s = drop_simple_quotes s' ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
-      let i = list_index s vars in
+      let i = List.index s vars in
       let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
       let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l
   | symbs, UnpBox (a,b) :: fmt ->
@@ -570,7 +570,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
   | symbs, (UnpCut _ as u) :: fmt ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | SProdList (m,sl) :: symbs, fmt ->
-      let i = list_index m vars in
+      let i = List.index m vars in
       let typ = List.nth typs (i-1) in
       let _,prec = precedence_of_entry_type from typ in
       let slfmt,fmt = read_recursive_format sl fmt in
@@ -889,7 +889,7 @@ let find_precedence lev etyps symbols =
 	  error "A left-recursive notation must have an explicit level."
 	else [],Option.get lev)
   | Terminal _ ::l when
-      (match list_last symbols with Terminal _ -> true |_ -> false)
+      (match List.last symbols with Terminal _ -> true |_ -> false)
       ->
       if lev = None then
 	([msg_info,strbrk "Setting notation at level 0."], 0)
@@ -1181,7 +1181,7 @@ let cache_scope_command o =
 
 let subst_scope_command (subst,(scope,o as x)) = match o with
   | ScopeClasses cl ->
-      let cl' = list_map_filter (subst_scope_class subst) cl in
+      let cl' = List.map_filter (subst_scope_class subst) cl in
       let cl' =
         if List.length cl = List.length cl' && List.for_all2 (==) cl cl' then cl
         else cl' in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 2a0f3c1671..b9783a9cb1 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -31,7 +31,7 @@ let trace s =
 let succfix (depth, fixrels) =
   (succ depth, List.map succ fixrels)
 
-let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
+let mkMetas n = List.tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
 let check_evars env evm =
   List.iter
@@ -80,7 +80,7 @@ let subst_evar_constr evs n idf t =
 	  *)
 	let args =
 	  let n = match chop with None -> 0 | Some c -> c in
-	  let (l, r) = list_chop n (List.rev (Array.to_list args)) in
+	  let (l, r) = List.chop n (List.rev (Array.to_list args)) in
 	    List.rev r
 	in
 	let args =
@@ -108,7 +108,7 @@ let subst_evar_constr evs n idf t =
 (** Substitute variable references in t using De Bruijn indices,
   where n binders were passed through. *)
 let subst_vars acc n t =
-  let var_index id = Util.list_index id acc in
+  let var_index id = Util.List.index id acc in
   let rec substrec depth c = match kind_of_term c with
     | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
     | _ -> map_constr_with_binders succ substrec depth c
@@ -146,7 +146,7 @@ open Tacticals
 
 let trunc_named_context n ctx =
   let len = List.length ctx in
-    list_firstn (len - n) ctx
+    List.firstn (len - n) ctx
 
 let rec chop_product n t =
   if n = 0 then Some t
@@ -547,13 +547,13 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype =
 	 fixpoints ?) *)
       let m = Term.nb_prod fixtype in
       let ctx = fst (decompose_prod_n_assum m fixtype) in
-	list_map_i (fun i _ -> i) 0 ctx
+	List.map_i (fun i _ -> i) 0 ctx
 
 let declare_mutual_definition l =
   let len = List.length l in
   let first = List.hd l in
   let fixdefs, fixtypes, fiximps =
-    list_split3
+    List.split3
       (List.map (fun x -> 
 	let subs, typ = (subst_body true x) in
 	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
@@ -571,14 +571,14 @@ let declare_mutual_definition l =
     match fixkind with
       | IsFixpoint wfl ->
 	  let possible_indexes =
-	    list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
+	    List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
 	  let indexes = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
-	    Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
+	    Some indexes, List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
       | IsCoFixpoint ->
-	  None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
+	  None, List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
   in
   (* Declare the recursive definitions *)
-  let kns = list_map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
+  let kns = List.map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
     Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 978329e137..487add3165 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -158,7 +158,7 @@ let subst_projection fid l c =
   c''
 
 let instantiate_possibly_recursive_type indsp paramdecls fields =
-  let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in
+  let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
   Termops.substl_rel_context (subst@[mkInd indsp]) fields
 
 (* We build projections *)
@@ -173,7 +173,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
-    list_fold_left3
+    List.fold_left3
       (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
 	let (sp_projs,subst) =
 	  match fi with
@@ -234,7 +234,7 @@ let structure_signature ctx =
       | (_,_,typ)::tl ->
 	  let ev = Evarutil.new_untyped_evar() in
 	  let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val typ) in
-	  let new_tl = Util.list_map_i
+	  let new_tl = Util.List.map_i
 	    (fun pos (n,c,t) -> n,c,
 	       Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) 1 tl in
 	  deps_to_evar evm new_tl in
@@ -280,7 +280,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
   rsp
 
 let implicits_of_context ctx =
-  list_map_i (fun i name ->
+  List.map_i (fun i name ->
     let explname =
       match name with
       | Name n -> Some n
@@ -346,7 +346,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 			       Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) 
 	  coers priorities 
 	in
-	  IndRef ind, (list_map3 (fun (id, _, _) b y -> (id, b, y))
+	  IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y))
 			 (List.rev fields) coers (Recordops.lookup_projections ind))
   in
   let ctx_context =
@@ -362,7 +362,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
       cl_props = fields;
       cl_projs = projs }
   in
-(*     list_iter3 (fun p sub pri -> *)
+(*     List.iter3 (fun p sub pri -> *)
 (*       if sub then match p with (_, _, Some p) -> declare_instance_cst true p pri | _ -> ()) *)
 (*       k.cl_projs coers priorities; *)
   add_class k; impl
@@ -389,7 +389,7 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
     | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
     | _ -> acc in
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (list_distinct allnames) then error "Two objects have the same name";
+  if not (List.distinct allnames) then error "Two objects have the same name";
   if not (kind = Class false) && List.exists ((<>) None) priorities then
     error "Priorities only allowed for type class substructures";
   (* Now, younger decl in params and fields is on top *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 18cef702c8..dc451fe050 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -153,9 +153,9 @@ let show_intro all =
     msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
   else
     try
-      let n = list_last l in
+      let n = List.last l in
       msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
-    with Failure "list_last" -> ()
+    with Failure "List.last" -> ()
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -174,7 +174,7 @@ let make_cases s =
 	Util.array_fold_right2
 	  (fun consname typ l ->
 	     let al = List.rev (fst (Term.decompose_prod typ)) in
-	     let al = Util.list_skipn np al in
+	     let al = Util.List.skipn np al in
 	     let rec rename avoid = function
 	       | [] -> []
 	       | (n,_)::l ->
@@ -217,8 +217,8 @@ let print_modules () =
   and loaded = Library.loaded_libraries () in
   (* we intersect over opened to preserve the order of opened since *)
   (* non-commutative operations (e.g. visibility) are done at import time *)
-  let loaded_opened = list_intersect opened loaded
-  and only_loaded = list_subtract loaded opened in
+  let loaded_opened = List.intersect opened loaded
+  and only_loaded = List.subtract loaded opened in
   str"Loaded and imported library files: " ++
   pr_vertical_list pr_dirpath loaded_opened ++ fnl () ++
   str"Loaded and not imported library files: " ++
@@ -289,7 +289,7 @@ let print_namespace ns =
       | MPfile dir -> Names.repr_dirpath dir
       | MPdot (mp,lbl) -> (Names.id_of_label lbl)::(list_of_modulepath mp)
     in
-    snd (Util.list_chop n (List.rev (list_of_modulepath mp)))
+    snd (Util.List.chop n (List.rev (list_of_modulepath mp)))
   in
   let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
   let print_kn kn =
@@ -817,7 +817,7 @@ let vernac_set_end_tac tac =
 
 let vernac_set_used_variables l =
   let l = List.map snd l in
-  if not (list_distinct l) then error "Used variables list contains duplicates";
+  if not (List.distinct l) then error "Used variables list contains duplicates";
   let vars = Environ.named_context (Global.env ()) in
   List.iter (fun id -> 
     if not (List.exists (fun (id',_,_) -> id = id') vars) then
@@ -905,7 +905,7 @@ let vernac_declare_arguments local r l nargs flags =
   let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in
   if List.exists ((<>) names) rest then
     error "All arguments lists must declare the same names.";
-  if not (Util.list_distinct (List.filter ((<>) Anonymous) names)) then
+  if not (Util.List.distinct (List.filter ((<>) Anonymous) names)) then
     error "Arguments names must be distinct.";
   let sr = smart_global r in
   let inf_names =
@@ -929,7 +929,7 @@ let vernac_declare_arguments local r l nargs flags =
     if List.exists (List.exists ((<>) None)) rest then
       error "Notation scopes can be given only once";
     if not extra_scope_flag then l, scopes else
-    let l, _ = List.split (List.map (list_chop (List.length inf_names)) l) in
+    let l, _ = List.split (List.map (List.chop (List.length inf_names)) l) in
     l, scopes in
   (* we interpret _ as the inferred names *)
   let l = if l = [[]] then l else
@@ -943,8 +943,8 @@ let vernac_declare_arguments local r l nargs flags =
     with Not_found -> false in
   let some_renaming_specified, implicits =
     if l = [[]] then false, [[]] else
-    Util.list_fold_map (fun sr il ->
-      let sr', impl = Util.list_fold_map (fun b -> function
+    Util.List.fold_map (fun sr il ->
+      let sr', impl = Util.List.fold_map (fun b -> function
         | (Anonymous, _,_, true, max), Name id -> assert false
         | (Name x, _,_, true, _), Anonymous ->
             error ("Argument "^string_of_id x^" cannot be declared implicit.")
@@ -953,7 +953,7 @@ let vernac_declare_arguments local r l nargs flags =
         | (Name iid, _,_, _, _), Name id -> b || iid <> id, None
         | _ -> b, None)
         sr (List.combine il inf_names) in
-      sr || sr', Util.list_map_filter (fun x -> x) impl)
+      sr || sr', Util.List.map_filter (fun x -> x) impl)
       some_renaming_specified l in
   if some_renaming_specified then
     if not (List.mem `Rename flags) then
@@ -969,8 +969,8 @@ let vernac_declare_arguments local r l nargs flags =
         with _ -> Some (Notation.find_delimiters_scope o k)) scopes in
   let some_scopes_specified = List.exists ((<>) None) scopes in
   let rargs =
-    Util.list_map_filter (function (n, true) -> Some n | _ -> None)
-      (Util.list_map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
+    Util.List.map_filter (function (n, true) -> Some n | _ -> None)
+      (Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
   if some_scopes_specified || List.mem `ClearScopes flags then
     vernac_arguments_scope local r scopes;
   if not some_implicits_specified && List.mem `DefaultImplicits flags then