4 files changed, 13 insertions, 10 deletions
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index aaf195a43..810603e45 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -40,7 +40,7 @@ type kind_of_formula=
   |Evaluable of evaluable_global_reference*constr
   |False
 
-type counter = bool -> int
+type counter = bool -> metavariable
 
 let constant path str ()=Coqlib.gen_constant "User" ["Init";path] str
 
@@ -167,7 +167,7 @@ type right_pattern =
     Rand
   | Ror 
   | Rforall
-  | Rexists of int*constr
+  | Rexists of metavariable*constr
   | Rarrow
   | Revaluable of evaluable_global_reference
       
@@ -189,7 +189,7 @@ type left_pattern=
     Lfalse    
   | Land of inductive
   | Lor of inductive 
-  | Lforall of int*constr
+  | Lforall of metavariable*constr
   | Lexists
   | Levaluable of evaluable_global_reference
   | LA of constr*left_arrow_pattern
@@ -202,6 +202,8 @@ type left_formula={id:global_reference;
     
 exception Is_atom of constr
 
+let meta_succ m = m+1
+
 let build_left_entry nam typ internal gl metagen=
   try 
     let pattern=
@@ -211,7 +213,7 @@ let build_left_entry nam typ internal gl metagen=
 	| And(i,_)         ->  Land i
 	| Or(i,_)          ->  Lor i
 	| Exists (_,_,_,_) ->  Lexists
-	| Forall (d,_) -> let m=1+(metagen false) in Lforall(m,d)
+	| Forall (d,_) -> let m=meta_succ(metagen false) in Lforall(m,d)
 	| Evaluable (egc,_) ->Levaluable egc 
 	| Arrow (a,b) ->LA (a, 
 			    match kind_of_formula a with
@@ -243,7 +245,7 @@ let build_right_entry typ gl metagen=
 	| And(_,_)        -> Rand
 	| Or(_,_)         -> Ror
 	| Exists (_,d,_,_) -> 
-	    let m=1+(metagen false) in Rexists(m,d) 
+	    let m=meta_succ(metagen false) in Rexists(m,d) 
 	| Forall (_,a) -> Rforall 
 	| Arrow (a,b) -> Rarrow 
 	| Evaluable (egc,_)->Revaluable egc in
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index 1e23d7c0b..89bd6d25f 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -32,7 +32,7 @@ type kind_of_formula=
   |Evaluable of Names.evaluable_global_reference * Term.constr
   |False
 
-type counter = bool -> int
+type counter = bool -> metavariable
 
 val construct_nhyps : inductive -> int array
 
@@ -49,7 +49,7 @@ type right_pattern =
     Rand
   | Ror 
   | Rforall
-  | Rexists of int*constr
+  | Rexists of metavariable*constr
   | Rarrow
   | Revaluable of Names.evaluable_global_reference
     
@@ -71,7 +71,7 @@ type left_pattern=
     Lfalse    
   | Land of inductive
   | Lor of inductive 
-  | Lforall of int*constr
+  | Lforall of metavariable*constr
   | Lexists
   | Levaluable of Names.evaluable_global_reference
   | LA of constr*left_arrow_pattern
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
index 5c0148d1f..e5ac4134f 100644
--- a/contrib/first-order/unify.ml
+++ b/contrib/first-order/unify.ml
@@ -15,6 +15,7 @@ open Tacmach
 open Term
 open Names
 open Termops
+open Pattern
 open Reductionops
 
 exception UFAIL of constr*constr
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
index 281e94063..90d3cb3f9 100644
--- a/contrib/first-order/unify.mli
+++ b/contrib/first-order/unify.mli
@@ -15,9 +15,9 @@ type instance=
     Real of constr*int (* instance*valeur heuristique*)
   | Phantom of constr (* domaine de quantification *)
 
-val unif_atoms : int -> constr -> constr -> constr -> instance option
+val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
   
-val give_right_instances : int -> constr -> (bool * constr) list -> 
+val give_right_instances : metavariable -> constr -> (bool * constr) list -> 
   Sequent.t -> (constr*int) list option
 
 val give_left_instances : Formula.left_formula list-> Sequent.t ->