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

6 files changed, 11 insertions, 11 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f3e414126b..0dbaccc336 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -396,7 +396,7 @@ let clenv_independent clenv =
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
 let check_bindings bl =
-  match list_duplicates (List.map pi2 bl) with
+  match List.duplicates (List.map pi2 bl) with
     | NamedHyp s :: _ ->
 	errorlabstrm ""
 	  (str "The variable " ++ pr_id s ++
@@ -464,7 +464,7 @@ exception NoSuchBinding
 
 let clenv_constrain_last_binding c clenv =
   let all_mvs = collect_metas clenv.templval.rebus in
-  let k = try list_last all_mvs with Failure _ -> raise NoSuchBinding in
+  let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
   clenv_assign_binding clenv k c
 
 let error_not_right_number_missing_arguments n =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index dcf1e4c733..53f5705a5a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -308,7 +308,7 @@ let collect_meta_variables c =
   List.rev (collrec false [] c)
 
 let check_meta_variables c =
-  if not (list_distinct (collect_meta_variables c)) then
+  if not (List.distinct (collect_meta_variables c)) then
     raise (RefinerError (NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
@@ -536,7 +536,7 @@ let prim_refiner r sigma goal =
             | _ -> error "Not enough products."
 	in
 	let (sp,_) = check_ind env n cl in
-	let firsts,lasts = list_chop j rest in
+	let firsts,lasts = List.chop j rest in
 	let all = firsts@(f,n,cl)::lasts in
      	let rec mk_sign sign = function
 	  | (f,n,ar)::oth ->
@@ -580,7 +580,7 @@ let prim_refiner r sigma goal =
 		  error ("All methods must construct elements " ^
 			  "in coinductive types.")
 	in
-	let firsts,lasts = list_chop j others in
+	let firsts,lasts = List.chop j others in
 	let all = firsts@(f,cl)::lasts in
      	List.iter (fun (_,c) -> check_is_coind env c) all;
         let rec mk_sign sign = function
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index f7d9446b51..ab80841d8b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -126,7 +126,7 @@ let solve_nth ?(with_end_tac=false) gi tac =
     Proof_global.run_tactic (Proofview.tclFOCUS gi gi tac) 
   with 
     | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
-    | Proofview.IndexOutOfRange | Failure "list_chop" -> 
+    | Proofview.IndexOutOfRange | Failure "List.chop" -> 
 	let msg = str "No such goal: " ++ int gi ++ str "." in
 	Errors.errorlabstrm "" msg
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0e2ac1ddef..79b5ae7310 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -112,7 +112,7 @@ let focus_sublist i j l =
   let (left,sub_right) = list_goto (i-1) l in
   let (sub, right) = 
     try 
-      Util.list_chop (j-i+1) sub_right 
+      Util.List.chop (j-i+1) sub_right 
     with Failure "list_chop" -> 
       Errors.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal")
   in
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 75a2ae8c38..c16e02b3fb 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -56,9 +56,9 @@ let cache_strategy (_,str) =
 
 let subst_strategy (subs,(local,obj)) =
   local,
-  list_smartmap
+  List.smartmap
     (fun (k,ql as entry) ->
-      let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+      let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in
       if ql==ql' then entry else (k,ql'))
     obj
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 910653ddb8..0652f19864 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -109,7 +109,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) =
   let ng = List.length gs in
   if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll =
-      (list_map_i (fun i ->
+      (List.map_i (fun i ->
         apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
 	0 gs) in
     (sigr,List.flatten gll)
@@ -123,7 +123,7 @@ let thensl_tac tac taci = thens3parts_tac [||] tac taci
 (* Apply [tac i] on the ith subgoal (no subgoals number check) *)
 let thensi_tac tac (sigr,gs) =
   let gll =
-    list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
+    List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
   (sigr, List.flatten gll)
 
 let then_tac tac = thensf_tac [||] tac