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)=