10 files changed, 22 insertions, 27 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index db1a46a035..c55040df03 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 106c469c62..3b6b711c0a 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/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 1e7da3250b..938bec25b9 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -65,11 +65,14 @@ let default_intuition_tac =
 let (set_default_solver, default_solver, print_default_solver) = 
   Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
 
-VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
-    set_default_solver 
-      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
-      (Tacintern.glob_tactic t) ]
+    fun ~atts ~st -> let open Vernacinterp in
+      set_default_solver
+        (Locality.make_section_locality atts.locality)
+        (Tacintern.glob_tactic t);
+        st
+  ]
 END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index f660ba7343..d462013353 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -11,7 +11,7 @@ open Formula
 open Sequent
 open Rules
 open Instances
-open Term
+open Constr
 open Tacmach.New
 open Tacticals.New
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index c2606dbe8e..3409471a7a 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.ml b/plugins/firstorder/rules.ml
index d6309b057f..1a6eba8c62 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -235,8 +235,8 @@ let constant str = Universes.constr_of_global
   @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
-  [AllOccurrences,EvalConstRef (fst (Term.destConst (constant "not")));
-   AllOccurrences,EvalConstRef (fst (Term.destConst (constant "iff")))]
+  [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not")));
+   AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))]
 
 let normalize_evaluables=
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index d8d4c1a38a..5c46f4cec2 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 05194164b0..ea2d076ed9 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 ca6079c8b0..7f4a6dd86a 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 d3e8aeee88..390aa8c85c 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