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

17 files changed, 85 insertions, 85 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5068552d17..be1e8e7017 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -280,7 +280,7 @@ let subst_path_atom subst p =
   | PathAny -> p
   | PathHints grs ->
     let gr' gr = fst (subst_global subst gr) in
-    let grs' = list_smartmap gr' grs in
+    let grs' = List.smartmap gr' grs in
       if grs' == grs then p else PathHints grs'
 
 let rec subst_hints_path subst hp =
@@ -393,7 +393,7 @@ module Hint_db = struct
 
   let add_list l db = List.fold_left (fun db k -> add_one k db) db l
 
-  let remove_sdl p sdl = list_smartfilter p sdl 
+  let remove_sdl p sdl = List.smartfilter p sdl 
   let remove_he st p (sl1, sl2, dn as he) =
     let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
       if sl1' == sl1 && sl2' == sl2 then he
@@ -402,7 +402,7 @@ module Hint_db = struct
   let remove_list grs db =
     let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in
     let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
-    let hintnopat = list_smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
+    let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
 
   let remove_one gr db = remove_list [gr] db
@@ -691,14 +691,14 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
     match hintlist with
     | CreateDB _ -> obj
     | AddTransparency (grs, b) ->
-	let grs' = list_smartmap (subst_evaluable_reference subst) grs in
+	let grs' = List.smartmap (subst_evaluable_reference subst) grs in
 	  if grs==grs' then obj else (local, name, AddTransparency (grs', b))
     | AddHints hintlist ->
-	let hintlist' = list_smartmap subst_hint hintlist in
+	let hintlist' = List.smartmap subst_hint hintlist in
 	  if hintlist' == hintlist then obj else
 	    (local,name,AddHints hintlist')
     | RemoveHints grs ->
-	let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in
+	let grs' = List.smartmap (fun x -> fst (subst_global subst x)) grs in
 	  if grs==grs' then obj else (local, name, RemoveHints grs')
     | AddCut path ->
       let path' = subst_hints_path subst path in
@@ -761,7 +761,7 @@ let add_extern pri pat tacast local dbname =
   let tacmetas = [] in
     match pat with
     | Some (patmetas,pat) ->
-	(match (list_subtract tacmetas patmetas) with
+	(match (List.subtract tacmetas patmetas) with
 	| i::_ ->
 	    errorlabstrm "add_extern"
 	      (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
@@ -859,7 +859,7 @@ let interp_hints h =
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
 	Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
-        list_tabulate (fun i -> let c = (ind,i+1) in
+        List.tabulate (fun i -> let c = (ind,i+1) in
 			 None, true, PathHints [ConstructRef c], mkConstruct c)
 	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
@@ -1054,10 +1054,10 @@ let unify_resolve_gen = function
 (* Util *)
 
 let expand_constructor_hints env lems =
-  list_map_append (fun (sigma,lem) ->
+  List.map_append (fun (sigma,lem) ->
     match kind_of_term lem with
     | Ind ind ->
-	list_tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
+	List.tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
     | _ ->
 	[prepare_hint env (sigma,lem)]) lems
 
@@ -1067,7 +1067,7 @@ let expand_constructor_hints env lems =
 let add_hint_lemmas eapply lems hint_db gl =
   let lems = expand_constructor_hints (pf_env gl) lems in
   let hintlist' =
-    list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
+    List.map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
   Hint_db.add_list hintlist' hint_db
 
 let make_local_hint_db ?ts eapply lems gl =
@@ -1076,7 +1076,7 @@ let make_local_hint_db ?ts eapply lems gl =
     | None -> Hint_db.transparent_state (searchtable_map "core") 
     | Some ts -> ts
   in
-  let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in
+  let hintlist = List.map_append (pf_apply make_resolve_hyp gl) sign in
   add_hint_lemmas eapply lems
     (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl
 
@@ -1271,7 +1271,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db gl =
 
 and my_find_search_nodelta db_list local_db hdc concl =
   List.map (fun hint -> (None,hint))
-    (list_map_append (hintmap_of hdc concl) (local_db::db_list))
+    (List.map_append (hintmap_of hdc concl) (local_db::db_list))
 
 and my_find_search mod_delta =
   if mod_delta then my_find_search_delta
@@ -1281,7 +1281,7 @@ and my_find_search_delta db_list local_db hdc concl =
   let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in
   let f = hintmap_of hdc concl in
     if occur_existential concl then
-      list_map_append
+      List.map_append
 	(fun db ->
 	  if Hint_db.use_dn db then
 	    let flags = flags_of_state (Hint_db.transparent_state db) in
@@ -1291,7 +1291,7 @@ and my_find_search_delta db_list local_db hdc concl =
 	      List.map (fun x -> (Some flags,x)) (f db))
 	(local_db::db_list)
     else
-      list_map_append (fun db ->
+      List.map_append (fun db ->
 	if Hint_db.use_dn db then
 	  let flags = flags_of_state (Hint_db.transparent_state db) in
 	    List.map (fun x -> (Some flags, x)) (f db)
@@ -1346,7 +1346,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
 
 let make_db_list dbnames =
   let use_core = not (List.mem "nocore" dbnames) in
-  let dbnames = list_remove "nocore" dbnames in
+  let dbnames = List.remove "nocore" dbnames in
   let dbnames = if use_core then "core"::dbnames else dbnames in
   let lookup db =
     try searchtable_map db with Not_found -> error_no_such_hint_database db
@@ -1361,7 +1361,7 @@ let trivial ?(debug=Off) lems dbnames gl =
 
 let full_trivial ?(debug=Off) lems gl =
   let dbnames = Hintdbmap.dom !searchtable in
-  let dbnames = list_remove "v62" dbnames in
+  let dbnames = List.remove "v62" dbnames in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
   let d = mk_trivial_dbg debug in
   tclTRY_dbg d
@@ -1454,7 +1454,7 @@ let default_auto = auto !default_search_depth [] []
 
 let delta_full_auto ?(debug=Off) mod_delta n lems gl =
   let dbnames = Hintdbmap.dom !searchtable in
-  let dbnames = list_remove "v62" dbnames in
+  let dbnames = List.remove "v62" dbnames in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
   let d = mk_auto_dbg debug in
   tclTRY_dbg d
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index d2d18c53b3..dfa94102d0 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -207,7 +207,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
   let base = try find_base rbase with _ -> HintDN.empty in
-  let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in
+  let max = try fst (Util.List.last (HintDN.find_all base)) with _ -> 0 in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 78df21a6d5..1eecb1eb30 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -159,7 +159,7 @@ and e_my_find_search db_list local_db hdc complete concl =
   let prods, concl = decompose_prod_assum concl in
   let nprods = List.length prods in
   let hintl =
-    list_map_append
+    List.map_append
       (fun db ->
 	if Hint_db.use_dn db then
 	  let flags = flags_of_state (Hint_db.transparent_state db) in
@@ -251,7 +251,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
       let hints =
 	if is_class then
 	  let hints = build_subclasses ~check:false env sigma (VarRef id) None in
-	    (list_map_append
+	    (List.map_append
 	       (fun (pri, c) -> make_resolves env sigma 
 		  (true,false,Flags.is_verbose()) pri c) 
 	       hints)
@@ -376,7 +376,7 @@ let hints_tac hints =
 			 (* Reorder with dependent subgoals. *)
 			 (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
 		   in
-		   let gls' = list_map_i
+		   let gls' = List.map_i
 		     (fun j (evar, g) ->
 			let info =
 			  { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
@@ -472,7 +472,7 @@ let cut_of_hints h =
 
 let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
   let cut = cut_of_hints hints in
-  { it = list_map_i (fun i g -> 
+  { it = List.map_i (fun i g -> 
     let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'} in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
 
@@ -779,7 +779,7 @@ END
 
 let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
   try 
-    let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
+    let dbs = List.map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
     let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
       eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
    with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 28840669f9..fd5fbe25ac 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -119,11 +119,11 @@ and e_my_find_search db_list local_db hdc concl =
   let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then
-      list_map_append (fun db ->
+      List.map_append (fun db ->
 	let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
 	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else
-      list_map_append (fun db ->
+      List.map_append (fun db ->
 	let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
 	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in
@@ -261,7 +261,7 @@ module SearchProblem = struct
 	       { depth = pred s.depth; tacres = res;
 		 dblist = s.dblist; last_tactic = pp; prev = ps;
 		 localdb =
-		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
+		   List.addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
 	  l
       in
       List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
@@ -364,7 +364,7 @@ let eauto ?(debug=Off) np lems dbnames =
 
 let full_eauto ?(debug=Off) n lems gl =
   let dbnames = current_db_names () in
-  let dbnames =  list_remove "v62" dbnames in
+  let dbnames =  List.remove "v62" dbnames in
   let db_list = List.map searchtable_map dbnames in
   tclTRY (e_search_auto debug n lems db_list) gl
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index a2ec6dfa56..32acc5af57 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -37,10 +37,10 @@ let introCaseAssumsThen tac ba =
   let n1 = List.length case_thin_sign in
   let n2 = List.length ba.branchnames in
   let (l1,l2),l3 =
-    if n1 < n2 then list_chop n1 ba.branchnames, []
+    if n1 < n2 then List.chop n1 ba.branchnames, []
     else
       (ba.branchnames, []),
-       if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in
+       if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in
   let introCaseAssums =
     tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in
   (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 7bc372ca93..f26eb10241 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -129,7 +129,7 @@ let solveEqBranch rectype g =
     let (eqonleft,op,lhs,rhs,_) = match_eqdec (pf_concl g) in
     let (mib,mip) = Global.lookup_inductive rectype in
     let nparams   = mib.mind_nparams in
-    let getargs l = list_skipn nparams (snd (decompose_app l)) in
+    let getargs l = List.skipn nparams (snd (decompose_app l)) in
     let rargs   = getargs rhs
     and largs   = getargs lhs in
     List.fold_right2
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f744b015ad..33eb7c6185 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -63,7 +63,7 @@ let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
 let fresh env id = next_global_ident_away id []
 
 let build_dependent_inductive ind (mib,mip) =
-  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,
        extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt
@@ -96,20 +96,20 @@ let get_sym_eq_data env ind =
   let (mib,mip as specif) = lookup_mind_specif env ind in
   if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
     error "Not an inductive type with a single constructor.";
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   if List.exists (fun (_,b,_) -> b <> None) realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
     error "Constructor must have no arguments"; (* This can be relaxed... *)
-  let params,constrargs = list_chop mib.mind_nparams constrargs in
+  let params,constrargs = List.chop mib.mind_nparams constrargs in
   if mip.mind_nrealargs > mib.mind_nparams then
     error "Constructors arguments must repeat the parameters.";
-  let _,params2 = list_chop (mib.mind_nparams-mip.mind_nrealargs) params in
+  let _,params2 = List.chop (mib.mind_nparams-mip.mind_nrealargs) params in
   let paramsctxt1,_ =
-    list_chop (mib.mind_nparams-mip.mind_nrealargs) mib.mind_params_ctxt in
-  if not (list_equal eq_constr params2 constrargs) then
+    List.chop (mib.mind_nparams-mip.mind_nrealargs) mib.mind_params_ctxt in
+  if not (List.equal eq_constr params2 constrargs) then
     error "Constructors arguments must repeat the parameters.";
   (* nrealargs_ctxt and nrealargs are the same here *)
   (specif,mip.mind_nrealargs,realsign,mib.mind_params_ctxt,paramsctxt1)
@@ -128,14 +128,14 @@ let get_non_sym_eq_data env ind =
   let (mib,mip as specif) = lookup_mind_specif env ind in
   if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
     error "Not an inductive type with a single constructor.";
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   if List.exists (fun (_,b,_) -> b <> None) realsign then
     error "Inductive equalities with local definitions in arity not supported";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
     error "Constructor must have no arguments";
-  let _,constrargs = list_chop mib.mind_nparams constrargs in
+  let _,constrargs = List.chop mib.mind_nparams constrargs in
   (specif,constrargs,realsign,mip.mind_nrealargs)
 
 (**********************************************************************)
@@ -679,7 +679,7 @@ let build_congr env (eq,refl) ind =
   if mip.mind_nrealargs <> 1 then
     error "Expect an inductive type with one predicate parameter.";
   let i = 1 in
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realsign,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   if List.exists (fun (_,b,_) -> b <> None) realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b4cb48285f..4d67fef006 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -397,7 +397,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids =
 	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
-	      Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl)
+	      Idset.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in
 	if cl.concl_occs = NoOccurrences then do_hyps else
@@ -532,15 +532,15 @@ let find_positions env sigma t1 t2 =
       | Construct sp1, Construct sp2
           when List.length args1 = mis_constructor_nargs_env env sp1
             ->
-	  let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in
+	  let sorts = List.intersect sorts (allowed_sorts env (fst sp1)) in
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if is_conv env sigma hd1 hd2 then
 	    let nrealargs = constructor_nrealargs env sp1 in
-	    let rargs1 = list_lastn nrealargs args1 in
-	    let rargs2 = list_lastn nrealargs args2 in
+	    let rargs1 = List.lastn nrealargs args1 in
+	    let rargs2 = List.lastn nrealargs args2 in
             List.flatten
-	      (list_map2_i (fun i -> findrec sorts ((sp1,i)::posn))
+	      (List.map2_i (fun i -> findrec sorts ((sp1,i)::posn))
 		0 rargs1 rargs2)
 	  else if List.mem InType sorts then (* see build_discriminator *)
 	    raise (DiscrFound (List.rev posn,sp1,sp2))
@@ -1495,7 +1495,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) gl =
     with PatternMatchingFailure -> failwith "caught"
   in
   let ids = map_succeed test (pf_hyps_types gl) in
-  let ids = list_uniquize ids in
+  let ids = List.uniquize ids in
   subst_gen flags.rewrite_dependent_proof ids gl
 
 (* Rewrite the first assumption for which the condition faildir does not fail
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index a6dcb9d585..bb35cedeae 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -319,7 +319,7 @@ let match_with_nodep_ind t =
 		if array_for_all nodep_constr mip.mind_nf_lc then
 		  let params=
 		    if mip.mind_nrealargs=0 then args else
-		      fst (list_chop mib.mind_nparams args) in
+		      fst (List.chop mib.mind_nparams args) in
 		    Some (hdapp,params,mip.mind_nrealargs)
 		else
 		  None
diff --git a/tactics/inv.ml b/tactics/inv.ml
index cb1ffb3856..189c73a167 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -111,7 +111,7 @@ let make_inv_predicate env sigma indf realargs id status concl =
   let nhyps = rel_context_length hyps in
   let env' = push_rel_context hyps env in
   let realargs' = List.map (lift nhyps) realargs in
-  let pairs = list_map_i (compute_eqn env' sigma nhyps) 0 realargs' in
+  let pairs = List.map_i (compute_eqn env' sigma nhyps) 0 realargs' in
   (* Now the arity is pushed, and we need to construct the pairs
    * ai,mkRel(n-i+1) *)
   (* Now, we can recurse down this list, for each ai,(mkRel k) whether to
@@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names gl =
         (fun id ->
            (tclTHEN
               (apply_term (mkVar id)
-                 (list_tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
+                 (List.tabulate (fun _ -> Evarutil.mk_new_meta()) neqns))
               reflexivity))])
   gl
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 5242d0f3e9..3031734fb7 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -187,7 +187,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     compute_first_inversion_scheme env sigma ind sort dep_option
   in
   assert
-    (list_subset
+    (List.subset
        (global_vars env invGoal)
        (ids_of_named_context (named_context invEnv)));
   (*
diff --git a/tactics/refine.ml b/tactics/refine.ml
index fc2da8d0a9..1cb4f01e22 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -348,7 +348,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
           | _ -> error "Recursive functions must have names."
 	in
 	let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
-	let firsts,lasts = list_chop j (Array.to_list fixes) in
+	let firsts,lasts = List.chop j (Array.to_list fixes) in
 	tclTHENS
 	  (tclTHEN
             (ensure_products (succ ni.(j)))
@@ -365,7 +365,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
           | _ -> error "Recursive functions must have names."
 	in
 	let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
-	let firsts,lasts = list_chop j (Array.to_list cofixes) in
+	let firsts,lasts = List.chop j (Array.to_list cofixes) in
 	tclTHENS
 	  (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
 	  (List.map (function
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f9aa1f0257..c36ab2f83a 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -725,7 +725,7 @@ let fold_match ?(force=false) env sigma c =
   in
   let app =
     let ind, args = Inductive.find_rectype env cty in
-    let pars, args = list_chop ci.ci_npar args in
+    let pars, args = List.chop ci.ci_npar args in
     let meths = List.map (fun br -> br) (Array.to_list brs) in
       applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
   in 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b0997c067d..4ce382df24 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -92,7 +92,7 @@ let catch_error call_trace tac g =
   | LtacLocated _ as e -> raise e
   | Loc.Exc_located (_,LtacLocated _) as e -> raise e
   | e ->
-    let (nrep,loc',c),tail = list_sep_last call_trace in
+    let (nrep,loc',c),tail = List.sep_last call_trace in
     let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
     if tail = [] then
       let loc = if loc = dloc then loc' else loc in
@@ -928,7 +928,7 @@ and intern_match_rule onlytac ist = function
       let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
       let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
       let ido,metas2,pat = intern_pattern ist lfun mp in
-      let metas = list_uniquize (metas1@metas2) in
+      let metas = List.uniquize (metas1@metas2) in
       let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
       Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
   | [] -> []
@@ -1329,7 +1329,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
       (*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*)
       let sigma, c = interp_fun ist env sigma x in
       sigma, [c] in
-  let sigma, l = list_fold_map try_expand_ltac_var sigma l in
+  let sigma, l = List.fold_map try_expand_ltac_var sigma l in
   sigma, List.flatten l
 
 let interp_constr_list ist env sigma c =
@@ -1541,7 +1541,7 @@ let interp_bindings ist env sigma = function
     let sigma, l = interp_open_constr_list ist env sigma l in   
     sigma, ImplicitBindings l
 | ExplicitBindings l ->
-    let sigma, l = list_fold_map (interp_binding ist env) sigma l in
+    let sigma, l = List.fold_map (interp_binding ist env) sigma l in
     sigma, ExplicitBindings l
 
 let interp_constr_with_bindings ist env sigma (c,bl) =
@@ -1556,8 +1556,8 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
 
 let loc_of_bindings = function
 | NoBindings -> Loc.ghost
-| ImplicitBindings l -> loc_of_glob_constr (fst (list_last l))
-| ExplicitBindings l -> pi1 (list_last l)
+| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
+| ExplicitBindings l -> pi1 (List.last l)
 
 let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) =
   let loc1 = loc_of_glob_constr c in
@@ -1982,7 +1982,7 @@ and eval_with_fail ist is_lazy goal tac =
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist gl llc u =
   let lref = ref ist.lfun in
-  let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg (dloc,b)))) llc in
+  let lve = List.map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg (dloc,b)))) llc in
   lref := lve@ist.lfun;
   let ist = { ist with lfun = lve@ist.lfun } in
   val_interp ist gl u
@@ -2069,7 +2069,7 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
           db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
 	  try
             let id_match = pi1 hyp_match in
-            let nextlhyps = list_remove_assoc_in_triple id_match lhyps_rest in
+            let nextlhyps = List.remove_assoc_in_triple id_match lhyps_rest in
             apply_hyps_context_rec (lfun@lids) lm nextlhyps tl
           with e when is_match_catchable e ->
 	    match_next_pattern find_next' in
@@ -2335,7 +2335,7 @@ and interp_atomic ist gl tac =
 	(h_vm_cast_no_check c_interp)
   | TacApply (a,ev,cb,cl) ->
       let sigma, l =
-        list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
+        List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
       in
       let tac = match cl with
         | None -> h_apply a ev
@@ -2435,7 +2435,7 @@ and interp_atomic ist gl tac =
       h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
   | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
       let sigma, l =
-        list_fold_map (fun sigma (c,(ipato,ipats)) ->
+        List.fold_map (fun sigma (c,(ipato,ipats)) ->
           let c = interp_induction_arg ist gl c in
           (sigma,(c,
             (Option.map (interp_intro_pattern ist gl) ipato,
@@ -2492,7 +2492,7 @@ and interp_atomic ist gl tac =
       let sigma, bl = interp_bindings ist env sigma bl in
       tclWITHHOLES ev (h_right ev) sigma bl
   | TacSplit (ev,_,bll) ->
-      let sigma, bll = list_fold_map (interp_bindings ist env) sigma bll in
+      let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
       tclWITHHOLES ev (h_split ev) sigma bll
   | TacAnyConstructor (ev,t) ->
       abstract_tactic (TacAnyConstructor (ev,t))
@@ -3142,7 +3142,7 @@ let add_tacdef local isrec tacl =
   let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
   let ist =
     {(make_empty_glob_sign()) with ltacrecvars =
-	if isrec then list_map_filter
+	if isrec then List.map_filter
 	  (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun
 	else []} in
   let gtacl =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index aaa75a4e26..f88530eec3 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -87,7 +87,7 @@ let lastHypId gl  = nthHypId 1 gl
 let lastHyp gl    = nthHyp 1 gl
 
 let nLastDecls n gl =
-  try list_firstn n (pf_hyps gl)
+  try List.firstn n (pf_hyps gl)
   with Failure _ -> error "Not enough hypotheses in the goal."
 
 let nLastHypsId n gl = List.map pi1 (nLastDecls n gl)
@@ -108,7 +108,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
 let onNLastHyps n tac   = onHyps (nLastHyps n) tac
 
 let afterHyp id gl =
-  fst (list_split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+  fst (List.split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
 
 (***************************************)
 (*           Clause Tacticals          *)
@@ -174,7 +174,7 @@ let fix_empty_or_and_pattern nv l =
      names and "[ ]" for no clause at all *)
   (* 2- More generally, we admit "[ ]" for any disjunctive pattern of
      arbitrary length *)
-  if l = [[]] then list_make nv [] else l
+  if l = [[]] then List.make nv [] else l
 
 let check_or_and_pattern_size loc names n =
   if List.length names <> n then
@@ -335,7 +335,7 @@ let make_elim_branch_assumptions ba gl =
       | (_, _) -> anomaly "make_elim_branch_assumptions"
   in
   makerec ([],[],[],[],[]) ba.branchsign
-    (try list_firstn ba.nassums (pf_hyps gl)
+    (try List.firstn ba.nassums (pf_hyps gl)
      with Failure _ -> anomaly "make_elim_branch_assumptions")
 
 let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
@@ -359,7 +359,7 @@ let make_case_branch_assumptions ba gl =
       | (_, _) -> anomaly "make_case_branch_assumptions"
   in
   makerec ([],[],[],[]) ba.branchsign
-    (try list_firstn ba.nassums (pf_hyps gl)
+    (try List.firstn ba.nassums (pf_hyps gl)
      with Failure _ -> anomaly "make_case_branch_assumptions")
 
 let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1ccb3ffdb2..b1a9c6732f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -857,7 +857,7 @@ let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause =
 let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl =
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
-    try match list_remove indmv (clenv_independent elimclause) with
+    try match List.remove indmv (clenv_independent elimclause) with
       | [a] -> a
       | _ -> failwith ""
     with Failure _ -> errorlabstrm "elimination_clause"
@@ -929,7 +929,7 @@ let descend_in_conjunctions tac exit c gl =
 	    let elim = pf_apply build_case_analysis_scheme gl ind false sort in
 	    NotADefinedRecordUseScheme elim in
 	tclFIRST
-	  (list_tabulate (fun i gl ->
+	  (List.tabulate (fun i gl ->
 	    match make_projection (project gl) params cstr sign elim i n c with
 	    | None -> tclFAIL 0 (mt()) gl
 	    | Some (p,pt) ->
@@ -1025,7 +1025,7 @@ let progress_with_clause flags innerclause clause =
   if ordered_metas = [] then error "Statement without assumptions.";
   let f mv =
     find_matching_clause (clenv_fchain mv ~flags clause) innerclause in
-  try list_try_find f ordered_metas
+  try List.try_find f ordered_metas
   with Failure _ -> error "Unable to unify."
 
 let apply_in_once_main flags innerclause (d,lbind) gl =
@@ -1164,7 +1164,7 @@ let specialize mopt (c,lbind) g =
       let nargs = List.length tstack in
       let tstack = match mopt with
 	| Some m ->
-	    if m < nargs then list_firstn m tstack else tstack
+	    if m < nargs then List.firstn m tstack else tstack
 	| None ->
 	    let rec chk = function
 	      | [] -> []
@@ -1565,8 +1565,8 @@ let generalize_dep ?(with_let=false) c gl =
 
 let generalize_gen_let lconstr gl =
   let newcl =
-    list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
-  apply_type newcl (list_map_filter (fun ((_,c,b),_) -> 
+    List.fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
+  apply_type newcl (List.map_filter (fun ((_,c,b),_) -> 
     if b = None then Some c else None) lconstr) gl
 
 let generalize_gen lconstr =
@@ -1753,7 +1753,7 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
     | Some occ ->
         subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in
   let lastlhyp =
-    if depdecls = [] then MoveLast else MoveAfter(pi1(list_last depdecls)) in
+    if depdecls = [] then MoveLast else MoveAfter(pi1(List.last depdecls)) in
   (depdecls,lastlhyp,ccl,out test)
 
 let letin_tac_gen with_eq name (sigmac,c) test ty occs gl =
@@ -1998,7 +1998,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
   let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in
   let prods, indtyp = decompose_prod typ0 in
   let argl = snd (decompose_app indtyp) in
-  let params = list_firstn nparams argl in
+  let params = List.firstn nparams argl in
   (* le gl est important pour ne pas préévaluer *)
   let rec atomize_one i avoid gl =
     if i<>nparams then
@@ -2031,7 +2031,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
 let find_atomic_param_of_ind nparams indtyp =
   let argl = snd (decompose_app indtyp) in
   let argv = Array.of_list argl in
-  let params = list_firstn nparams argl in
+  let params = List.firstn nparams argl in
   let indvars = ref Idset.empty in
   for i = nparams to (Array.length argv)-1 do
     match kind_of_term argv.(i) with
@@ -2749,8 +2749,8 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	    (* Check again conclusion *)
 	    let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f = IndArg in
 	    let ind_is_ok =
-	      list_equal eq_constr
-		(list_lastn scheme.nargs indargs)
+	      List.equal eq_constr
+		(List.lastn scheme.nargs indargs)
 		(extended_rel_list 0 scheme.args) in
 	    if not (ccl_arg_ok & ind_is_ok) then
 	      error_ind_scheme "the conclusion of"
@@ -2895,11 +2895,11 @@ let recolle_clenv nparams lid elimclause gl =
   let nidargs = List.length lidargs in
   (* parameters correspond to first elts of lid. *)
   let clauses_params =
-    list_map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i))
+    List.map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i))
       0 lidparams in
   (* arguments correspond to last elts of lid. *)
   let clauses_args =
-    list_map_i
+    List.map_i
       (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(nmv-nidargs+i))
       0 lidargs in
   let clauses = clauses_params@clauses_args in
@@ -3087,7 +3087,7 @@ let clear_unselected_context id inhyps cls gl =
 	      (* erase if not selected and dependent on id or selected hyps *)
 	      let test id = occur_var_in_decl (pf_env gl) id d in
 	      if List.exists test (id::inhyps) then Some id' else None in
-	  let ids = list_map_filter to_erase (pf_hyps gl) in
+	  let ids = List.map_filter to_erase (pf_hyps gl) in
 	  thin ids gl
       | None -> tclIDTAC gl
 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 9696696684..fdfc2b7834 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -173,7 +173,7 @@ let flatten_contravariant_disj flags ist =
           typ with
   | Some (_,args) ->
       let hyp = valueIn (VConstr ([],hyp)) in
-      iter_tac (list_map_i (fun i arg ->
+      iter_tac (List.map_i (fun i arg ->
 	let typ = valueIn (VConstr ([],mkArrow arg c)) in
 	let i = Tacexpr.Integer i in
 	<:tactic<