diff options
| author | Pierre-Marie Pédrot | 2014-09-06 19:43:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-06 22:21:35 +0200 |
| commit | a74074a8133ad954dff54bee190dbaa5332564a0 (patch) | |
| tree | debf20cc3836c2c8433a93aa5e26a3ac26c20540 /plugins/pluginsbyte.itarget | |
| parent | 489964b94ba1bb2cc6f36674b7eb439f8126e377 (diff) | |
Proper interpretation function for tauto.
Instead of passing glob tactics through the infamous globTacticIn hack and
antiquotation feature of the Ltac syntax, we put them in the interpretation
environment as closures. This should be used everywhere to get rid of this
buggy antiquotation syntax.
This fixes bug #2800.
Diffstat (limited to 'plugins/pluginsbyte.itarget')
0 files changed, 0 insertions, 0 deletions