diff options
| author | Arnaud Spiwack | 2014-10-22 18:12:52 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | 212dec2878f1dfe2a5fa06ac7722df06ef5dd5a6 (patch) | |
| tree | ee3ca73172b8f2605a1cae1946e63fbdb342c50e /plugins | |
| parent | 9826a9f56b11125d6d0b540546f04dc12f845090 (diff) | |
Info: tactic notations (TacAlias) print their names.
Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions