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

7 files changed, 36 insertions, 36 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8ea4be631c..0796930fca 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -93,7 +93,7 @@ let observe_tac s = observe_tac_stream (str s)
 
 let list_chop ?(msg="") n l =
   try
-    list_chop n l
+    List.chop n l
   with Failure (msg') ->
     failwith (msg ^ msg')
 
@@ -319,7 +319,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	      )
     in
     let new_type_of_hyp,ctxt_size,witness_fun =
-      list_fold_left_i
+      List.fold_left_i
 	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
 	   try
 	     let witness = Intmap.find i sub in
@@ -1168,7 +1168,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		typess
 	    in
 	    let pte_to_fix,rev_info =
-	      list_fold_left_i
+	      List.fold_left_i
 		(fun i (acc_map,acc_info) (pte,_,_) ->
 		   let infos = info_array.(i) in
 		   let type_args,_ = decompose_prod infos.types in
@@ -1557,7 +1557,7 @@ let prove_principle_for_gen
 (* 	     str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
 (* 	     str "npost_rec_arg := " ++ int npost_rec_arg ); *)
   let (post_rec_arg,pre_rec_arg) =
-    Util.list_chop npost_rec_arg princ_info.args
+    Util.List.chop npost_rec_arg princ_info.args
   in
   let rec_arg_id =
     match List.rev post_rec_arg with
@@ -1624,7 +1624,7 @@ let prove_principle_for_gen
 	  Elim.h_decompose_and (mkVar hid);
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
-	     tcc_list := List.rev (list_subtract new_hyps (hid::hyps));
+	     tcc_list := List.rev (List.subtract new_hyps (hid::hyps));
 	     if !tcc_list = []
 	     then
 	       begin
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index e2dc149b09..f2eb4b23cf 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -88,7 +88,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     Nameops.out_name x,None,compose_prod real_args (mkSort new_sort)
   in
   let new_predicates =
-    list_map_i
+    List.map_i
       change_predicate_sort
       0
       princ_type_info.predicates
@@ -252,7 +252,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let pre_res =
     replace_vars
-      (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
+      (List.map_i (fun i id -> (id, mkRel i)) 1 ptes_vars)
       (lift (List.length ptes_vars) pre_res)
   in
   it_mkProd_or_LetIn
@@ -460,7 +460,7 @@ let get_funs_constant mp dp =
       let first_params = List.hd l_params  in
       List.iter
 	(fun params ->
-	   if not (list_equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params)
+	   if not (List.equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params)
 	   then error "Not a mutal recursive block"
 	)
 	l_params
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d11c01672a..1c21934495 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -89,7 +89,7 @@ let combine_results
   in (* and then we flatten the map *)
   {
     result = List.concat pre_result;
-    to_avoid = list_union res1.to_avoid res2.to_avoid
+    to_avoid = List.union res1.to_avoid res2.to_avoid
   }
 
 
@@ -269,7 +269,7 @@ let make_discr_match_el  =
   end
 *)
 let make_discr_match_brl i =
-  list_map_i
+  List.map_i
     (fun j (_,idl,patl,_) ->
        if j=i
        then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
@@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let case_pats = build_constructors_of_type ind [] in
 	assert (Array.length case_pats = 2);
 	let brl =
-	  list_map_i
+	  List.map_i
 	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
 	    0
 	    [lhs;rhs]
@@ -748,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr
 	{
 	  result = List.concat (List.map (fun r -> r.result) results);
 	  to_avoid =
-	    List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
+	    List.fold_left (fun acc r -> List.union acc r.to_avoid) [] results
 	}
 
 and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid
@@ -818,7 +818,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
       	let those_pattern_preconds =
 	  (List.flatten
 	    (
-	      list_map3
+	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
 		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
@@ -977,7 +977,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let mib,_ = Global.lookup_inductive ind in
 		    let nparam = mib.Declarations.mind_nparams in
 		    let params,arg' =
-		      ((Util.list_chop nparam args'))
+		      ((Util.List.chop nparam args'))
 		    in
 		    let rt_typ =
 		       GApp(Loc.ghost,
@@ -1000,7 +1000,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      match kind_of_term eq'_as_constr with
 			| App(_,[|_;_;ty;_|]) ->
 			    let ty = Array.to_list (snd (destApp ty)) in
-			    let ty' = snd (Util.list_chop nparam ty) in
+			    let ty' = snd (Util.List.chop nparam ty) in
 			    List.fold_left2
 			      (fun acc var_as_constr arg ->
 				 if isRel var_as_constr
@@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
   let l = ref [] in
   let _ =
     try
-      list_iter_i
+      List.iter_i
 	(fun i ((n,nt,is_defined) as param) ->
 	   if array_for_all
 	     (fun l ->
@@ -1362,7 +1362,7 @@ let do_build_inductive
   in
   let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
     let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list  =
-      (snd (list_chop nrel_params funargs))
+      (snd (List.chop nrel_params funargs))
     in
     List.fold_right
       (fun (n,t,is_defined) acc ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 52562fb374..18b2bbe2f7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -21,7 +21,7 @@ let is_rec_info scheme_info =
       Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
   in
-  Util.list_fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
+  Util.List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
 
 let choose_dest_or_ind scheme_info =
     if is_rec_info scheme_info
@@ -337,7 +337,7 @@ let generate_principle  on_error
 	in
 	let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in
 	let _ =
-	  list_map_i
+	  List.map_i
 	    (fun i x ->
 	       let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in
 	       let princ_type = Typeops.type_of_constant (Global.env()) princ
@@ -392,7 +392,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	if List.length names = 1 then 1
 	else error "Recursive argument must be specified"
       | Some wf_arg ->
-	  list_index (Name wf_arg) names
+	  List.index (Name wf_arg) names
   in
   let unbounded_eq =
     let f_app_args =
@@ -516,7 +516,7 @@ let decompose_lambda_n_assum_constr_expr =
 	    (n - nal_length) 
 	    (Constrexpr.CLambdaN(lambda_loc,bl,e'))
   	else
-	  let nal_keep,nal_expr = list_chop n nal in 
+	  let nal_keep,nal_expr = List.chop n nal in 
 	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
 	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
 	  )
@@ -548,7 +548,7 @@ let decompose_prod_n_assum_constr_expr =
 	    (if bl = [] then e' else (Constrexpr.CLambdaN(lambda_loc,bl,e')))
   	else
 	  (* let _ = Pp.msgnl (str "second case") in  *)
-	  let nal_keep,nal_expr = list_chop n nal in 
+	  let nal_keep,nal_expr = List.chop n nal in 
 	  (List.rev (Constrexpr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
 	   Constrexpr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
 	  )
@@ -585,7 +585,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	    let lnal' = List.length nal' in 
 	    if lnal' >= lnal 
 	    then 
-	      let old_nal',new_nal' = list_chop lnal nal' in 
+	      let old_nal',new_nal' = List.chop lnal nal' in 
 	      rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl' 
 		(if new_nal' = [] && rest = []
 		 then  typ' 
@@ -593,7 +593,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 		 then CProdN(Loc.ghost,rest,typ')
 		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
 	    else 
-	      let captured_nal,non_captured_nal = list_chop lnal' nal in 
+	      let captured_nal,non_captured_nal = List.chop lnal' nal in 
 	      rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal))
 		bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ'))
 	  | _ -> assert false
@@ -789,7 +789,7 @@ let rec chop_n_arrow n t =
 		    else
 		      let new_t' =
 			Constrexpr.CProdN(Loc.ghost,
-					((snd (list_chop n nal)),k,t'')::nal_ta',t')
+					((snd (List.chop n nal)),k,t'')::nal_ta',t')
 		      in
 		      raise (Stop new_t')
 		in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2f6a6a7d7b..1d1089a549 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -370,7 +370,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       in
       (* in fact we must also add the parameters to the constructor args *)
       let constructor_args g =
-	let params_id = fst (list_chop princ_infos.nparams args_names) in
+	let params_id = fst (List.chop princ_infos.nparams args_names) in
 	(List.map mkVar params_id)@((constructor_args g))
       in
       (* We then get the constructor corresponding to this branch and
@@ -446,7 +446,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	)
 	lemmas_types_infos
     in
-    let param_names = fst (list_chop princ_infos.nparams args_names) in
+    let param_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar param_names in
     let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
     (* The bindings of the principle
@@ -611,7 +611,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       in
       (* in fact we must also add the parameters to the constructor args *)
       let constructor_args =
-	let params_id = fst (list_chop princ_infos.nparams args_names) in
+	let params_id = fst (List.chop princ_infos.nparams args_names) in
 	(List.map mkVar params_id)@(List.rev constructor_args)
       in
       (* We then get the constructor corresponding to this branch and
@@ -669,7 +669,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	g
     in
     (* end of branche proof *)
-    let param_names = fst (list_chop princ_infos.nparams args_names) in
+    let param_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar param_names in
     let lemmas = Array.to_list (Array.map (fun c -> applist(c,params)) lemmas) in
     (* The bindings of the principle
@@ -996,7 +996,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       ]
 	g
     in
-    let params_names = fst (list_chop princ_infos.nparams args_names) in
+    let params_names = fst (List.chop princ_infos.nparams args_names) in
     let params = List.map mkVar params_names in
     tclTHENSEQ
       [ tclMAP h_intro (args_names@[res;hres]);
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 4fe22a3543..21c0d86a4f 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -165,11 +165,11 @@ let array_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b array): 'a =
       let res = f !i acc x in i := !i + 1; res)
     acc arr
 
-(* Like list_chop but except that [i] is the size of the suffix of [l]. *)
+(* Like List.chop but except that [i] is the size of the suffix of [l]. *)
 let list_chop_end i l =
   let size_prefix = List.length l -i in
   if size_prefix < 0 then failwith "list_chop_end"
-  else list_chop size_prefix l
+  else List.chop size_prefix l
 
 let list_fold_lefti (f: int -> 'a -> 'b -> 'a) (acc:'a) (arr:'b list): 'a =
   let i = ref 0 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 14d9b7fcb0..8b0fc27397 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -705,7 +705,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     (try
       (tclTHENS
 	 destruct_tac
-	 (list_map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
+	 (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
 	 ))
     with 
       | UserError("Refiner.thensn_tac3",_) 
@@ -1014,7 +1014,7 @@ let compute_terminate_type nb_args func =
 	  Array.of_list
 	    (lift 5 a_arrow_b:: mkRel 3::
 	       constr_of_global func::mkRel 1::
-	       List.rev (list_map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
+	       List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
 	    )
 	 )
   in
@@ -1044,7 +1044,7 @@ let termination_proof_header is_mes input_type ids args_id relation
       let nargs = List.length args_id in
       let pre_rec_args =
 	List.rev_map
-	  mkVar (fst (list_chop (rec_arg_num - 1) args_id))
+	  mkVar (fst (List.chop (rec_arg_num - 1) args_id))
       in
       let relation = substl pre_rec_args relation in
       let input_type = substl pre_rec_args input_type in
@@ -1297,7 +1297,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 		    (Elim.h_decompose_and (mkVar hid))
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
-		       lid := List.rev (list_subtract ids' ids);
+		       lid := List.rev (List.subtract ids' ids);
 		       if !lid = [] then lid := [hid];
 		       tclIDTAC g
 		    )