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

2 files changed, 13 insertions, 13 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 5e128bc423..f2f978ccdf 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -57,7 +57,7 @@ let intern_hyp iconstr globs = function
       Hprop (intern_statement iconstr globs st)
 
 let intern_hyps iconstr globs hyps =
-  snd (list_fold_map (intern_hyp iconstr) globs hyps)
+  snd (List.fold_map (intern_hyp iconstr) globs hyps)
 
 let intern_cut intern_it globs cut=
   let nglobs,nstat=intern_it globs cut.cut_stat in
@@ -74,10 +74,10 @@ let intern_hyp_list args globs =
   let intern_one globs (loc,(id,opttyp)) =
     (add_var id globs),
     (loc,(id,Option.map (intern_constr globs) opttyp)) in
-  list_fold_map intern_one globs args
+  List.fold_map intern_one globs args
 
 let intern_suffices_clause globs (hyps,c) =
-  let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in
+  let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in
     nglobs,(nhyps,intern_constr_or_thesis nglobs c)
 
 let intern_fundecl args body globs=
@@ -340,7 +340,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
 	(fun (loc,(id,_)) ->
 	   GVar (loc,id)) params in
     let dum_args=
-      list_tabulate
+      List.tabulate
 	(fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false)))
 	oib.Declarations.mind_nrealargs in
       glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 31e15081b2..1a0d05047e 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -857,7 +857,7 @@ let build_per_info etype casee gls =
     match etype with
 	ET_Induction -> mind.mind_nparams_rec,Some (snd ind)
       | _ -> mind.mind_nparams,None in
-  let params,real_args = list_chop nparams args in
+  let params,real_args = List.chop nparams args in
   let abstract_obj c body =
     let typ=pf_type_of gls c in
       lambda_create env (typ,subst_term c body) in
@@ -953,7 +953,7 @@ let rec tree_of_pats ((id,_) as cpl) pats =
 		    let nexti i ati =
 		      if i = pred cnum then
 			let nargs =
-			  list_map_i (fun j a -> (a,ati.(j))) 0 args in
+			  List.map_i (fun j a -> (a,ati.(j))) 0 args in
 			  Some (Idset.singleton id,
 				tree_of_pats cpl (nargs::rest_args::stack))
 		      else None
@@ -998,7 +998,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 			  let nexti i ati =
 			    if i = pred cnum then
 			      let nargs =
-				list_map_i (fun j a -> (a,ati.(j))) 0 args in
+				List.map_i (fun j a -> (a,ati.(j))) 0 args in
 				Some (Idset.add id ids,
 				      add_branch cpl (nargs::rest_args::stack)
 					(skip_args t ids (Array.length ati)))
@@ -1013,7 +1013,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 			  let mapi i ati bri =
 			    if i = pred cnum then
 			      let nargs =
-				list_map_i (fun j a -> (a,ati.(j))) 0 args in
+				List.map_i (fun j a -> (a,ati.(j))) 0 args in
 				append_branch cpl 0
 				  (nargs::rest_args::stack) bri
 			    else bri in
@@ -1051,7 +1051,7 @@ let thesis_for obj typ per_info env=
     errorlabstrm "thesis_for"
       ((Printer.pr_constr_env env obj) ++ spc () ++
 	 str"cannot give an induction hypothesis (wrong inductive type).") in
-  let params,args = list_chop per_info.per_nparams all_args in
+  let params,args = List.chop per_info.per_nparams all_args in
   let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
     errorlabstrm "thesis_for"
       ((Printer.pr_constr_env env obj) ++ spc () ++
@@ -1182,7 +1182,7 @@ let hrec_for fix_id per_info gls obj_id =
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
   let ind = destInd cind in assert (ind=per_info.per_ind);
-  let params,args= list_chop per_info.per_nparams all_args in
+  let params,args= List.chop per_info.per_nparams all_args in
   assert begin
     try List.for_all2 eq_constr params per_info.per_params with
         Invalid_argument _ -> false end;
@@ -1203,8 +1203,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	  match List.assoc id args with
 	      [None,br_args] -> 
 		let all_metas = 
-		  list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
-		let param_metas,hyp_metas = list_chop nparams all_metas in
+		  List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps)  in
+		let param_metas,hyp_metas = List.chop nparams all_metas in
 		  tclTHEN
 		    (tclDO nhrec introf)
 		    (tacnext 
@@ -1221,7 +1221,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let ctyp=pf_type_of gls casee in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
 	let _ = assert (destInd hd = ind) in (* just in case *)
-	let params,real_args = list_chop nparams all_args in
+	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
 	  let typ=pf_type_of gls c in
 	    lambda_create env (typ,subst_term c body) in