7 files changed, 12 insertions, 20 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index db1a46a03..c55040df0 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -8,7 +8,7 @@
 
 open Hipattern
 open Names
-open Term
+open Constr
 open EConstr
 open Vars
 open Termops
@@ -39,7 +39,7 @@ exception Is_atom of constr
 let meta_succ m = m+1
 
 let rec nb_prod_after n c=
-  match kind_of_term c with
+  match Constr.kind c with
     | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
 	1+(nb_prod_after 0 b)
     | _ -> 0
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 106c469c6..3b6b711c0 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 open Globnames
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index c2606dbe8..3409471a7 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -24,7 +24,7 @@ open Misctypes
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
-        let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
+        let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
 	match inst1,inst2 with
 	    Phantom(d1),Phantom(d2)->
 	      (cmp d1 d2)
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index d8d4c1a38..5c46f4cec 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
-open EConstr
 open Names
+open Constr
+open EConstr
 open Globnames
 
 type tactic = unit Proofview.tactic
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 05194164b..ea2d076ed 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -54,13 +54,7 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
-module OrderedConstr=
-struct
-  type t=Term.constr
-  let compare=Term.compare
-end
-
-type h_item = global_reference * (int*Term.constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module Hitem=
 struct
@@ -70,13 +64,13 @@ struct
     if c = 0 then
       let cmp (i1, c1) (i2, c2) =
         let c = Int.compare i1 i2 in
-        if c = 0 then OrderedConstr.compare c1 c2 else c
+        if c = 0 then Constr.compare c1 c2 else c
       in
       Option.compare cmp co1 co2
     else c
 end
 
-module CM=Map.Make(OrderedConstr)
+module CM=Map.Make(Constr)
 
 module History=Set.Make(Hitem)
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index ca6079c8b..7f4a6dd86 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -10,11 +10,9 @@ open EConstr
 open Formula
 open Globnames
 
-module OrderedConstr: Set.OrderedType with type t=Term.constr
+module CM: CSig.MapS with type key=Constr.t
 
-module CM: CSig.MapS with type key=Term.constr
-
-type h_item = global_reference * (int*Term.constr) option
+type h_item = global_reference * (int*Constr.t) option
 
 module History: Set.S with type elt = h_item
 
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index d3e8aeee8..390aa8c85 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
+open Constr
 open EConstr
 
 exception UFAIL of constr*constr