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

5 files changed, 8 insertions, 8 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 7abb4dc527..f4cc397bcc 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -142,7 +142,7 @@ let build_atoms gl metagen side cciterm =
 	  let g i _ (_,_,t) =
 	    build_rec env polarity (lift i t) in
 	  let f l =
-	    list_fold_left_i g (1-(List.length l)) () l in
+	    List.fold_left_i g (1-(List.length l)) () l in
 	    if polarity && (* we have a constant constructor *)
 	      array_exists (function []->true|_->false) v
 	    then trivial:=true;
@@ -152,7 +152,7 @@ let build_atoms gl metagen side cciterm =
 	  let v =(ind_hyps 1 i l gl).(0) in
 	  let g i _ (_,_,t) =
 	    build_rec (var::env) polarity (lift i t) in
-	    list_fold_left_i g (2-(List.length l)) () v
+	    List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
 	  let var=mkMeta (metagen true) in
 	    build_rec (var::env) polarity b
@@ -224,7 +224,7 @@ let build_formula side nam typ gl metagen=
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
 		  | Exists (i,l) ->
-		      let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in
+		      let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in
 			Rexists(m,d,trivial)
 		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e3367b4c22..414afad467 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -112,7 +112,7 @@ let mk_open_instance id gl m t=
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
-  let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in
+  let revt=substl (List.tabulate (fun i->mkRel (m-i)) m) t in
   let rec aux n avoid=
     if n=0 then [] else
       let nid=(fresh_id avoid var_id gl) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 37d9edef86..7acabaaa4c 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -129,7 +129,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
        let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
 	 it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
-       let newhyps=list_tabulate myterm lp in
+       let newhyps=List.tabulate myterm lp in
 	 tclIFTHENELSE
 	   (tclTHENLIST
 	      [generalize newhyps;
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 6d00e8d9fb..c648939bb0 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -191,9 +191,9 @@ let empty_seq depth=
    depth=depth}
 
 let expand_constructor_hints =
-  list_map_append (function
+  List.map_append (function
     | IndRef ind ->
-	list_tabulate (fun i -> ConstructRef (ind,i+1))
+	List.tabulate (fun i -> ConstructRef (ind,i+1))
 	  (Inductiveops.nconstructors ind)
     | gr ->
 	[gr])
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 33ea0ac8a0..c3726f1a83 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -124,7 +124,7 @@ let unif_atoms i dom t1 t2=
     | Not_found ->Some (Phantom dom)
 
 let renum_metas_from k n t= (* requires n = max (free_rels t) *)
-  let l=list_tabulate (fun i->mkMeta (k+i)) n in
+  let l=List.tabulate (fun i->mkMeta (k+i)) n in
     substl l t
 
 let more_general (m1,t1) (m2,t2)=