diff options
| author | herbelin | 2013-02-21 16:39:34 +0000 |
|---|---|---|
| committer | herbelin | 2013-02-21 16:39:34 +0000 |
| commit | 760e1e8ae75b168183e56248e0f8ee1a59a09265 (patch) | |
| tree | 4949ce052fb2131b82c31ae9f35090e3ad6e3552 /pretyping | |
| parent | 52fc3e2c5dbab866e37cf02f77e0422c344a6faa (diff) | |
A slightly more efficient test of well-typedness of restriction of
evars (though this might be slighty more costly).
This incidentally solves Appel's part of bug #2830 even though a
conceptual problem around the interaction of unification with the
proof engine has to be solved. Indeed, what to do when unification,
called as part of a tactic, solves or refines the current goal by side
effect. Somehow, unifyTerms or tclEVARS should take this possibility
into consideration, either by forbidding the refinement of the current
goal by side effect, or by acknowledging this refinement by producing
new subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16232 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -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 a63f1b1c84..f29d982c2d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -783,7 +783,7 @@ let eq_filter f1 f2 = let closure_of_filter evd evk filter = let evi = Evd.find_undefined evd evk in - let vars = collect_vars (evar_concl evi) 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 |