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 /plugins/syntax/string_syntax.ml | |
| 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 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions