3 files changed, 4 insertions, 7 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 2d5ea9536c..fb363b9393 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,7 +15,6 @@ open EConstr
 open Vars
 open Util
 open Declarations
-open Globnames
 
 module RelDecl = Context.Rel.Declaration
 
@@ -124,7 +123,7 @@ type side = Hyp | Concl | Hint
 
 let no_atoms = (false,{positive=[];negative=[]})
 
-let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
+let dummy_id=GlobRef.VarRef (Id.of_string "_") (* "_" cannot be parsed *)
 
 let build_atoms env sigma metagen side cciterm =
   let trivial =ref false
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index bdf339a488..e134562702 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -15,12 +15,11 @@ open Rules
 open Instances
 open Tacmach.New
 open Tacticals.New
-open Globnames
 
 let update_flags ()=
   let open TransparentState in
   let f accu coe = match coe.Classops.coe_value with
-    | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
+    | Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
     | _ -> accu
   in
   let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index f3a16cd13e..79386f7ac9 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -20,7 +20,6 @@ open Proofview.Notations
 open Termops
 open Formula
 open Sequent
-open Globnames
 
 module NamedDecl = Context.Named.Declaration
 
@@ -48,7 +47,7 @@ let wrap n b continue seq =
 	      List.exists (occur_var_in_decl env sigma id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula env sigma Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
+              add_formula env sigma Hyp (GlobRef.VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
   let seq1=aux n nc [] in
   let seq2=if b then
     add_formula env sigma Concl dummy_id (pf_concl gls) seq1 else seq1 in
@@ -56,7 +55,7 @@ let wrap n b continue seq =
   end
 
 let clear_global=function
-    VarRef id-> clear [id]
+  | GlobRef.VarRef id-> clear [id]
   | _->tclIDTAC
 
 (* connection rules *)