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

1 files changed, 9 insertions, 9 deletions

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