diff options
| author | Hugo Herbelin | 2016-04-22 12:02:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:49 +0200 |
| commit | 7e613daf7c71a4180725bddb40151c2b5a6348f4 (patch) | |
| tree | 0fa960e2b4fc7dd78f4398462cad29a6ccfb6a18 /ltac | |
| parent | d28c1d7d908fe9d5fc719d58433a6b87c12390ba (diff) | |
When interpreting "match goal with ... end" in ltac, expand evars by
need at matching time rather than eagerly at the beginning of the call
to "match".
To be done for other constructs too, e.g. "match term with ... endp".
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacinterp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index e8dee7a001..b742bb328d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1530,7 +1530,9 @@ and interp_match ist lz constr lmr = (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = - Ftactic.nf_enter { enter = begin fun gl -> + Ftactic.enter { enter = begin fun gl -> + (* Because match_goal will lazily whd_evar when necessary *) + let gl = Proofview.Goal.assume gl in let sigma = project gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in |