From 3cd718c8f7b48bae776b62ffafa1aa7e18218ed4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Jan 2015 16:15:39 +0100
Subject: Fixing 48509b61 which improved unification as expected but actually
 not using the intended test. By fixing the intended test, the need for a
 delta-expansion resulting from this commit in PFsection6.v (line 1255) of
 ssreflect disappears.

---
 pretyping/evarsolve.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f8518beaa6..078117fbd0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -870,7 +870,7 @@ let closure_of_filter evd evk = function
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
-  let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> isRel c in
+  let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in
   let newfilter = Filter.map_along test filter (evar_context evi) in
   if Filter.equal newfilter (evar_filter evi) then None else Some newfilter
 
-- 
cgit v1.2.3