diff options
| author | Hugo Herbelin | 2015-05-08 12:41:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-08 16:27:32 +0200 |
| commit | 3bcfff90470ef079b5e711ef72db28b670eeacd0 (patch) | |
| tree | aaa3171909154982d0abe300f8987f72bcff8df8 /plugins | |
| parent | 32a9a4e3656e581af41c26f48f63ed1daec331d8 (diff) | |
A more user-friendly naming of variables of ltac names defined by
TACTIC EXTEND (based on user-given name).
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions