diff options
-rw-r--r-- | plugins/firstorder/unify.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 6c82a9685..299a0054a 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -89,9 +89,8 @@ let unif t1 t2= let value i t= let add x y= if x<0 then y else if y<0 then x else x+y in - let tref=mkMeta i in let rec vaux term= - if term=tref then 0 else + if isMeta term && destMeta term = i then 0 else let f v t=add v (vaux t) in let vr=fold_constr f (-1) term in if vr<0 then -1 else vr+1 in |