diff options
| author | Hugo Herbelin | 2015-01-03 16:15:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-03 18:14:06 +0100 |
| commit | 3cd718c8f7b48bae776b62ffafa1aa7e18218ed4 (patch) | |
| tree | 7443173e4ef9e74642bc5f1c1082934efffd2ba3 | |
| parent | 43f01df26be3a3a0f731aeb0728b1b43188a1743 (diff) | |
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.
| -rw-r--r-- | pretyping/evarsolve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |