diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 18:13:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 18:23:54 +0200 |
| commit | 7525890df67fe711e2d3d63846ddb1e988d0812b (patch) | |
| tree | accc5678b182a6a65eb4ebd291f93da7f5779c27 /tactics/tactics.ml | |
| parent | 4afe5e4385fc303010a4afd6040565ccd54291a9 (diff) | |
Fixing bug #2818.
Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
Diffstat (limited to 'tactics/tactics.ml')
0 files changed, 0 insertions, 0 deletions