diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 21:45:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 21:45:42 +0000 |
| commit | 8646837a56962c9319d7fd428a72223b947ac141 (patch) | |
| tree | def8a1a298aff5763c1d65d435654db9be143b14 | |
| parent | eec75e3814818ec96ac1045c2dd63e242620dcfe (diff) | |
Fixing unfolding of local definitions during unification that appeared
with commit r16233. This commit added a more precise filtering of
variables on which an evar was allowed to be dependent, but) but it
also broke some Ssreflect scripts. The reason why that filtering was
incorrectly applied, sometimes, to local definitions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16346 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarsolve.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 50fc91e31..b3a2e2a39 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -786,9 +786,8 @@ 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 ids = List.map pi1 (evar_context evi) in - let test id b = b || Id.Set.mem id vars in - let newfilter = List.map2 test ids filter in + let test (id,c,_) b = b || Idset.mem id vars || c <> None in + let newfilter = List.map2 test (evar_context evi) filter in if eq_filter newfilter (evar_filter evi) then None else Some newfilter let restrict_hyps evd evk filter candidates = |