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/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d11c01672..1c2193449 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 ->