diff options
| author | Arnaud Spiwack | 2014-09-05 09:08:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-05 18:26:00 +0200 |
| commit | 2fcc458af16bbebb9748cb4220237e74452059fc (patch) | |
| tree | 170d751cda948d6dbf564fe50e5e755828261e1d /dev | |
| parent | 8a1f5056e144c12e5e67aa7ac328cd65e730ede2 (diff) | |
Adds an identifier context in pretying's Ltac context.
Binder names are interpreted as the Ltac specified one if available.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions