3 files changed, 10 insertions, 7 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 1e7da3250..938bec25b 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 f660ba734..d46201335 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/rules.ml b/plugins/firstorder/rules.ml
index d6309b057..1a6eba8c6 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 ->