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

11 files changed, 60 insertions, 60 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 950edc5a3..306fbfad9 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -75,7 +75,7 @@ let local_binder_loc = function
 
 let local_binders_loc bll =
   if bll = [] then Loc.ghost else
-  Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+  Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (List.last bll))
 
 (** Pseudo-constructors *)
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 272845d07..0ce8a8aac 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -257,7 +257,7 @@ let is_same_type c d =
 (* mapping patterns to cases_pattern_expr                                *)
 
 let add_patt_for_params ind l =
-    Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
+    Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -276,7 +276,7 @@ let drop_implicits_in_patt cst nb_expl args =
      in
      if nb_expl = 0 then aux impl_data
      else
-       let imps = list_skipn_at_least nb_expl (select_stronger_impargs impl_st) in
+       let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
        impls_fit [] (imps,args)
 
 let has_curly_brackets ntn =
@@ -355,7 +355,7 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
   let nb_params = Inductiveops.inductive_nparams ind in
   List.exists (fun (_,impls) ->
     (List.length impls >= nb_params) &&
-      let params,args = Util.list_chop nb_params impls in
+      let params,args = Util.List.chop nb_params impls in
       (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
   ) impl_st
 
@@ -570,8 +570,8 @@ let explicitize loc inctx impl (cf,f) args =
 	  let f' = match f with CRef f -> f | _ -> assert false in
 	  CAppExpl (loc,(ip,f'),args)
 	else
-	  let (args1,args2) = list_chop i args in
-	  let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in
+	  let (args1,args2) = List.chop i args in
+	  let (impl1,impl2) = if impl=[] then [],[] else List.chop i impl in
 	  let args1 = exprec 1 (args1,impl1) in
 	  let args2 = exprec (i+1) (args2,impl2) in
 	  CApp (loc,(Some (List.length args1),f),args1@args2)
@@ -617,7 +617,7 @@ let rec remove_coercions inctx = function
       (try match Classops.hide_coercion r with
 	  | Some n when n < nargs && (inctx or n+1 < nargs) ->
 	      (* We skip a coercion *)
-	      let l = list_skipn n args in
+	      let l = List.skipn n args in
 	      let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
               (* Recursively remove the head coercions *)
 	      let a' = remove_coercions true a in
@@ -893,17 +893,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 	let (t,args,argsscopes,argsimpls) = match t,n with
 	  | GApp (_,f,args), Some n
 	      when List.length args >= n ->
-	      let args1, args2 = list_chop n args in
+	      let args1, args2 = List.chop n args in
               let subscopes, impls =
                 match f with
                 | GRef (_,ref) ->
 	          let subscopes =
-		    try list_skipn n (find_arguments_scope ref) with _ -> [] in
+		    try List.skipn n (find_arguments_scope ref) with _ -> [] in
 	          let impls =
 		    let impls =
 		      select_impargs_size
 		        (List.length args) (implicits_of_global ref) in
-		    try list_skipn n impls with _ -> [] in
+		    try List.skipn n impls with _ -> [] in
                   subscopes,impls
                 | _ ->
                   [], [] in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 86998c210..7ad1327fd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -193,7 +193,7 @@ let empty_internalization_env = Idmap.empty
 let compute_explicitable_implicit imps = function
   | Inductive params ->
       (* In inductive types, the parameters are fixed implicit arguments *)
-      let sub_impl,_ = list_chop (List.length params) imps in
+      let sub_impl,_ = List.chop (List.length params) imps in
       let sub_impl' = List.filter is_status_implicit sub_impl in
       List.map name_of_implicit sub_impl'
   | Recursive | Method | Variable ->
@@ -206,7 +206,7 @@ let compute_internalization_data env ty typ impl =
   (ty, expls_impl, impl, compute_arguments_scope typ)
 
 let compute_internalization_env env ty =
-  list_fold_left3
+  List.fold_left3
     (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map)
     empty_internalization_env
 
@@ -674,7 +674,7 @@ let find_appl_head_data = function
       when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
       x,List.map (drop_first_implicits n) (implicits_of_global ref),
-      list_skipn_at_least n (find_arguments_scope ref),[]
+      List.skipn_at_least n (find_arguments_scope ref),[]
   | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
@@ -708,7 +708,7 @@ let intern_qualid loc qid intern env lvar args =
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
       if List.length args < nids then error_not_enough_arguments loc;
-      let args1,args2 = list_chop nids args in
+      let args1,args2 = List.chop nids args in
       check_no_explicitation args1;
       let subst = make_subst ids (List.map fst args1) in
       subst_aconstr_in_glob_constr loc intern lvar (subst,[],[]) ([],env) c, args2
@@ -766,15 +766,15 @@ let find_remaining_scopes pl1 pl2 ref =
   let len_pl2 = List.length pl2 in
   let impl_list = if len_pl1 = 0
     then select_impargs_size len_pl2 impls_st
-    else list_skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
+    else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
   let allscs = find_arguments_scope ref in
-  let scope_list = list_skipn_at_least len_pl1 allscs in
+  let scope_list = List.skipn_at_least len_pl1 allscs in
   let rec aux = function
     |[],l -> l
     |_,[] -> []
     |h::t,_::tt when is_status_implicit h -> aux (t,tt)
     |_::t,h::tt -> h :: aux (t,tt)
-  in ((try list_firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
+  in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
       simple_adjust_scopes len_pl2 (aux (impl_list,scope_list)))
 
 let product_of_cases_patterns ids idspl =
@@ -800,7 +800,7 @@ let rec has_duplicate = function
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs =
- Loc.merge (fst (List.hd lhs)) (fst (list_last lhs))
+ Loc.merge (fst (List.hd lhs)) (fst (List.last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -815,7 +815,7 @@ let check_number_of_pattern loc n l =
   if n<>p then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
 
 let check_or_pat_variables loc ids idsl =
-  if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
+  if List.exists (fun ids' -> not (List.eq_set ids ids')) idsl then
     user_err_loc (loc, "", str
     "The components of this disjunctive pattern must bind the same variables.")
 
@@ -832,7 +832,7 @@ let check_constructor_length env loc cstr len_pl pl0 =
 let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
   let impl_list = if len_pl1 = 0
     then select_impargs_size (List.length pl2) impls_st
-    else list_skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
+    else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
   let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
   let rec aux i = function
     |[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in
@@ -870,7 +870,7 @@ let chop_params_pattern loc ind args with_letin =
     then fst (Inductiveops.inductive_nargs ind)
     else Inductiveops.inductive_nparams ind in
   assert (nparams <= List.length args);
-  let params,args = list_chop nparams args in
+  let params,args = List.chop nparams args in
   List.iter (function PatVar(_,Anonymous) -> ()
     | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params;
   args
@@ -883,7 +883,7 @@ let find_constructor loc add_params ref =
     |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c
       then fst (Inductiveops.inductive_nargs ind)
       else Inductiveops.inductive_nparams ind in
-		     Util.list_make nb ([],[([],PatVar(Loc.ghost,Anonymous))])
+		     Util.List.make nb ([],[([],PatVar(Loc.ghost,Anonymous))])
     |None -> []) cstr
 
 let find_pattern_variable = function
@@ -1033,7 +1033,7 @@ let drop_notations_pattern looked_for =
 	      looked_for g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
-	      let pats1,pats2 = list_chop nvars pats in
+	      let pats1,pats2 = List.chop nvars pats in
 	      let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
 	      let idspl1 = List.map (in_not loc env (subst,[]) []) args in
 	      let (_,argscs) = find_remaining_scopes pats1 pats2 g in
@@ -1283,7 +1283,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-	  try list_index0 iddef lf
+	  try List.index0 iddef lf
           with Not_found ->
 	    raise (InternalizationError (locid,UnboundFixName (false,iddef)))
 	in
@@ -1308,7 +1308,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	     in
 	       ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
         let idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
-	     let env'' = list_fold_left_i (fun i en name -> 
+	     let env'' = List.fold_left_i (fun i en name -> 
 					     let (_,bli,tyi,_) = idl_temp.(i) in
 					     let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
 					       push_name_env lvar (impls_type_list ~args:fix_args tyi)
@@ -1324,7 +1324,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
         let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
-          try list_index0 iddef lf
+          try List.index0 iddef lf
           with Not_found ->
 	    raise (InternalizationError (locid,UnboundFixName (true,iddef)))
 	in
@@ -1335,7 +1335,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
             (List.rev rbl,
              intern_type env' ty,env')) dl in
 	let idl = array_map2 (fun (_,_,_,bd) (b,c,env') ->
-	     let env'' = list_fold_left_i (fun i en name ->
+	     let env'' = List.fold_left_i (fun i en name ->
 					     let (bli,tyi,_) = idl_tmp.(i) in
 					     let cofix_args =  List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
 	       push_name_env lvar (impls_type_list ~args:cofix_args tyi)
@@ -1407,7 +1407,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  match cargs with
 	    | None -> user_err_loc (loc, "intern", str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = list_make n (CHole (loc, None)) in
+		let pars = List.make n (CHole (loc, None)) in
 		let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
 	  intern env app
 	end
@@ -1440,7 +1440,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 			  List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
 			  [Loc.ghost,[],thepats, (* "|p1,..,pn" *)
 			   Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
-			   Loc.ghost,[],list_make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
+			   Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
 			   GHole(Loc.ghost,Evar_kinds.ImpossibleCase) (* "=> _" *)]))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
@@ -1553,7 +1553,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 		  ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
 	      |_ -> assert false in
 	  let _,args_rel =
-	    list_chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
+	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
 	  canonize_args args_rel l (Idset.elements forbidden_names_for_gen) [] [] in
 	match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal)
     | None ->
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 94cb91749..531ca5bf4 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -45,7 +45,7 @@ let gen_constant_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = qualid_of_string s in
   let all = Nametab.locate_extended_all qualid in
-  let all = list_uniquize (list_map_filter global_of_extended all) in
+  let all = List.uniquize (List.map_filter global_of_extended all) in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> constr_of_global x
@@ -73,7 +73,7 @@ let check_required_library d =
   if not (Library.library_is_loaded dir) then
     if not current_dir then
 (* Loading silently ...
-    let m, prefix = list_sep_last d' in
+    let m, prefix = List.sep_last d' in
     read_library
      (Loc.ghost,make_qualid (make_dirpath (List.rev prefix)) m)
 *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index c9e18c15e..101645dfc 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -174,7 +174,7 @@ let dump_constraint ((loc, n), _, _) sec ty =
 let dump_modref loc mp ty =
   if dump () then
     let (dp, l) = Lib.split_modpath mp in
-    let l = if l = [] then l else Util.list_drop_last l in
+    let l = if l = [] then l else Util.List.drop_last l in
     let fp = Names.string_of_dirpath dp in
     let mp = Names.string_of_dirpath (Names.make_dirpath l) in
     let bl,el = interval loc in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3057cef34..c4cc38a56 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -316,6 +316,6 @@ let implicits_of_glob_constr ?(with_products=true) l =
       | GLetIn (loc, na, t, b) -> aux i b
       | GRec (_, fix_kind, nas, args, tys, bds) ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
-       list_fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
+       List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
       | _ -> []
   in aux 1 l
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 1e7d84c96..ba5c68a5d 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -77,7 +77,7 @@ let lookup_qualid (modtype:bool) qid =
   in
   let rec find_module_prefix dir n =
     if n<0 then raise Not_found;
-    let dir',dir'' = list_chop n dir in
+    let dir',dir'' = List.chop n dir in
     let id',dir''' =
       match dir'' with
 	| hd::tl -> hd,tl
diff --git a/interp/notation.ml b/interp/notation.ml
index 6a574a56e..46a06b700 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -125,7 +125,7 @@ let open_scope i (_,(local,op,sc)) =
       | _ -> sc
     in
     scope_stack :=
-      if op then sc :: !scope_stack else list_except sc !scope_stack
+      if op then sc :: !scope_stack else List.except sc !scope_stack
 
 let cache_scope o =
   open_scope 1 o
@@ -285,7 +285,7 @@ let check_required_module loc sc (sp,d) =
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
     str ("Cannot interpret in "^sc^" without requiring first module "
-    ^(list_last d)^"."))
+    ^(List.last d)^"."))
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -402,7 +402,7 @@ let interp_notation loc ntn local_scopes =
 let isGApp = function GApp _ -> true | _ -> false
 
 let uninterp_notations c =
-  list_map_append (fun key -> Gmapl.find key !notations_key_table)
+  List.map_append (fun key -> Gmapl.find key !notations_key_table)
     (glob_constr_keys c)
 
 let uninterp_cases_pattern_notations c =
@@ -554,7 +554,7 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
         match subst_scope_class subst cl with
         | Some cl'  as ocl' when cl' != cl -> ocl'
         | _ -> ocl in
-  let cls' = list_smartmap subst_cl cls in
+  let cls' = List.smartmap subst_cl cls in
   let scl' = merge_scope (List.map find_scope_class_opt cls') scl in
   let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
   (ArgsScopeNoDischarge,r',scl'',cls')
@@ -576,7 +576,7 @@ let rebuild_arguments_scope (req,r,l,_) =
 	(* Add to the manually given scopes the one found automatically
            for the extra parameters of the section *)
 	let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
-	let l1,_ = list_chop (List.length l' - List.length l) l' in
+	let l1,_ = List.chop (List.length l' - List.length l) l' in
 	(req,r,l1@l,cls)
 
 type arguments_scope_obj =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index bd3ba4274..13356445f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -33,7 +33,7 @@ let rec cases_pattern_fold_map loc g e = function
       let e',na' = g e na in e', PatVar (loc,na')
   | PatCstr (_,cstr,patl,na) ->
       let e',na' = g e na in
-      let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in
+      let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
       e', PatCstr (loc,cstr,patl',na')
 
 let rec subst_glob_vars l = function
@@ -86,18 +86,18 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
       let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
-	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
+	  List.fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
 	(loc,idl,patl,f e rhs)) eqnl in
       GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
-      let e',nal = list_fold_map g e nal in
+      let e',nal = List.fold_map g e nal in
       let e'',na = g e na in
       GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
   | NIf (c,(na,po),b1,b2) ->
       let e',na = g e na in
       GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | NRec (fk,idl,dll,tl,bl) ->
-      let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
+      let e,dll = array_fold_map (List.fold_map (fun e (na,oc,b) ->
 	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = array_fold_map (to_id g) e idl in
@@ -144,7 +144,7 @@ let on_true_do b f c = if b then (f c; b) else b
 let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2
   | GVar (_,v1), GVar (_,v2) -> on_true_do (v1 = v2) add (Name v1)
-  | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2
+  | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & List.for_all2eq f l1 l2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1
   | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
       on_true_do (f ty1 ty2 & f c1 c2) add na1
@@ -182,7 +182,7 @@ let compare_recursive_parts found f (iterator,subc) =
       (* We found the pattern, but there are extra arguments *)
       (* (this allows e.g. alternative (recursive) notation of application) *)
       assert (!terminator = None); terminator := Some term;
-      list_for_all2eq aux l1 l2
+      List.for_all2eq aux l1 l2
   | GVar (_,x), GVar (_,y) when x<>y ->
       (* We found the position where it differs *)
       let lassoc = (!terminator <> None) in
@@ -335,7 +335,7 @@ let rec subst_pat subst pat =
   | PatVar _ -> pat
   | PatCstr (loc,((kn,i),j),cpl,n) ->
       let kn' = subst_ind subst kn
-      and cpl' = list_smartmap (subst_pat subst) cpl in
+      and cpl' = List.smartmap (subst_pat subst) cpl in
         if kn' == kn && cpl' == cpl then pat else
           PatCstr (loc,((kn',i),j),cpl',n)
 
@@ -350,7 +350,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NApp (r,rl) ->
       let r' = subst_notation_constr subst bound r
-      and rl' = list_smartmap (subst_notation_constr subst bound) rl in
+      and rl' = List.smartmap (subst_notation_constr subst bound) rl in
 	if r' == r && rl' == rl then raw else
 	  NApp(r',rl')
 
@@ -386,7 +386,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NCases (sty,rtntypopt,rl,branches) ->
       let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
-      and rl' = list_smartmap
+      and rl' = List.smartmap
         (fun (a,(n,signopt) as x) ->
 	  let a' = subst_notation_constr subst bound a in
 	  let signopt' = Option.map (fun ((indkn,i),nal as z) ->
@@ -394,9 +394,9 @@ let rec subst_notation_constr subst bound raw =
 	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
-      and branches' = list_smartmap
+      and branches' = List.smartmap
                         (fun (cpl,r as branch) ->
-                           let cpl' = list_smartmap (subst_pat subst) cpl
+                           let cpl' = List.smartmap (subst_pat subst) cpl
                            and r' = subst_notation_constr subst bound r in
                              if cpl' == cpl && r' == r then branch else
                                (cpl',r'))
@@ -423,7 +423,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NRec (fk,idl,dll,tl,bl) ->
       let dll' =
-	array_smartmap (list_smartmap (fun (na,oc,b as x) ->
+	array_smartmap (List.smartmap (fun (na,oc,b as x) ->
 	  let oc' =  Option.smartmap (subst_notation_constr subst bound) oc in
 	  let b' =  subst_notation_constr subst bound b in
 	  if oc' == oc && b' == b then x else (na,oc',b'))) dll in
@@ -619,9 +619,9 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
 	if n1 < n2 then
-	  let l21,l22 = list_chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
+	  let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
 	else if n1 > n2 then
-	  let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
+	  let l11,l12 = List.chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
 	else f1,l1, f2, l2 in
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
@@ -710,7 +710,7 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
   match_in u alp metas sigma rhs1 rhs2
 
 let match_notation_constr u c (metas,pat) =
-  let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
+  let vars = List.split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
   let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
   let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
   (* Reorder canonically the substitution *)
@@ -734,7 +734,7 @@ let match_notation_constr u c (metas,pat) =
 let add_patterns_for_params ind l =
   let mib,_ = Global.lookup_inductive ind in
   let nparams = mib.Declarations.mind_nparams in
-    Util.list_addn nparams (PatVar (Loc.ghost,Anonymous)) l
+    Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
 
 let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
   try
@@ -758,7 +758,7 @@ let rec match_cases_pattern metas sigma a1 a2 =
       then
 	raise No_match
       else
-	let l1',more_args = Util.list_chop le2 l1 in
+	let l1',more_args = Util.List.chop le2 l1 in
 	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
   | r1, NList (x,_,iter,termin,lassoc) ->
       (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas)
@@ -781,7 +781,7 @@ let match_ind_pattern metas sigma ind pats a2 =
       then
 	raise No_match
       else
-	let l1',more_args = Util.list_chop le2 pats in
+	let l1',more_args = Util.List.chop le2 pats in
 	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
   |_ -> raise No_match
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 259ffa171..7a2d4bfe7 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -77,7 +77,7 @@ let revert_reserved_type t =
   try
     let l = Gmapl.find (constr_key t) !reserve_revtable in
     let t = Detyping.detype false [] [] t in
-    list_try_find
+    List.try_find
       (fun (pat,id) ->
 	try let _ = Notation_ops.match_notation_constr false t ([],pat) in Name id
 	with Notation_ops.No_match -> failwith "") l
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e717e1747..abdde1f54 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -158,7 +158,7 @@ let split_at_annot bl na =
   | Some (loc, id) ->
       let rec aux acc = function
 	| LocalRawAssum (bls, k, t) as x :: rest ->
-	    let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in
+	    let l, r = List.split_when (fun (loc, na) -> na = Name id) bls in
 	      if r = [] then aux (x :: acc) rest
 	      else
 		(List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc),