diff options
| author | Arnaud Spiwack | 2014-09-15 16:46:08 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-15 17:17:35 +0200 |
| commit | 83ebacdb7f307451fc801637224c911eb0da9fea (patch) | |
| tree | b8677fbc66d6bef4c62cbbb8995ec585a704b6d3 /interp/implicit_quantifiers.ml | |
| parent | 27e2e43b93491727096b9d1fb20f66cfc71ae320 (diff) | |
Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].
All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions