3 files changed, 7 insertions, 5 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 2d7a3e37b7..b13580bc03 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -233,7 +233,7 @@ let ll_forall_tac prod backtrack id continue seq=
 
 (* special for compatibility with old Intuition *)
 
-let constant str = Universes.constr_of_global
+let constant str = UnivGen.constr_of_global
   @@ Coqlib.coq_reference "User" ["Init";"Logic"] str
 
 let defined_connectives=lazy
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 0c752d4a48..2a527da9be 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -229,7 +229,9 @@ let extend_with_auto_hints env sigma l seq =
 
 let print_cmap map=
   let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index b869c04a21..d63fe9d799 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open Util
-open Term
+open Constr
 open EConstr
 open Vars
 open Termops
@@ -56,12 +56,12 @@ let unif evd t1 t2=
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
 		if Int.Set.is_empty (free_rels evd t) &&
-		  not (dependent evd (EConstr.mkMeta i) t) then
+                  not (occur_metavariable evd i t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
 		if Int.Set.is_empty (free_rels evd t) &&
-		  not (dependent evd (EConstr.mkMeta i) t) then
+                  not (occur_metavariable evd i t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige