5 files changed, 15 insertions, 12 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 4e3ba57308..516b04ea21 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -13,23 +13,21 @@ open Formula
 open Sequent
 open Rules
 open Instances
-open Constr
 open Tacmach.New
 open Tacticals.New
+open Globnames
 
 let update_flags ()=
-  let predref=ref Names.Cpred.empty in
-  let f coe=
-    try
-      let kn= fst (destConst (Classops.get_coercion_value coe)) in
-	predref:=Names.Cpred.add kn !predref
-    with DestKO -> ()
+  let f acc coe =
+    match coe.Classops.coe_value with
+    | ConstRef c -> Names.Cpred.add c acc
+    | _ -> acc
   in
-    List.iter f (Classops.coercions ());
+    let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
     red_flags:=
     CClosure.RedFlags.red_add_transparent
       CClosure.betaiotazeta
-      (Names.Id.Pred.full,Names.Cpred.complement !predref)
+      (Names.Id.Pred.full,Names.Cpred.complement pred)
 
 let ground_tac solver startseq =
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 85f4939560..286021d68e 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -38,7 +38,7 @@ let compare_gr id1 id2 =
   if id1==id2 then 0 else
     if id1==dummy_id then 1
     else if id2==dummy_id then -1
-    else Globnames.RefOrdered.compare id1 id2
+    else GlobRef.Ordered.compare id1 id2
 
 module OrderedInstance=
 struct
diff --git a/plugins/firstorder/plugin_base.dune b/plugins/firstorder/plugin_base.dune
new file mode 100644
index 0000000000..bcbb99d9fc
--- /dev/null
+++ b/plugins/firstorder/plugin_base.dune
@@ -0,0 +1,5 @@
+(library
+ (name ground_plugin)
+ (public_name coq.plugins.ground)
+ (synopsis "Coq's first order logic solver plugin")
+ (libraries coq.plugins.ltac))
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b13580bc03..3ae777cc9a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -34,7 +34,7 @@ type lseqtac= GlobRef.t -> seqtac
 type 'a with_backtracking = tactic -> 'a
 
 let wrap n b continue seq =
-  Proofview.Goal.nf_enter begin fun gls ->
+  Proofview.Goal.enter begin fun gls ->
   Control.check_for_interrupt ();
   let nc = Proofview.Goal.hyps gls in
   let env=pf_env gls in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2a527da9be..5958fe8203 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -62,7 +62,7 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    let c = Globnames.RefOrdered.compare id1 id2 in
+    let c = GlobRef.Ordered.compare id1 id2 in
     if c = 0 then
       let cmp (i1, c1) (i2, c2) =
         let c = Int.compare i1 i2 in