From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/firstorder/unify.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder/unify.ml')

diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 24fd8dd88f..e1adebe8dc 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -55,12 +55,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 (occur_term evd (EConstr.mkMeta i) t) then
+		  not (dependent evd (EConstr.mkMeta 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 (occur_term evd (EConstr.mkMeta i) t) then
+		  not (dependent evd (EConstr.mkMeta 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
-- 
cgit v1.2.3