diff options
| author | Arnaud Spiwack | 2014-10-24 18:56:13 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | 53c3b382b4ca82e4589d2f5e574df688ab7957de (patch) | |
| tree | 4c9ee68e074589e5dc10706c78b651ba61a49b27 /plugins | |
| parent | 212dec2878f1dfe2a5fa06ac7722df06ef5dd5a6 (diff) | |
Info: print name of calls to Ltac constants ([TacCall]).
Some particular care needed to be taken to print aliases properly.
The printing of argument is just the generic printer for [genarg]. The trouble is that (apart from being incomplete), it does not know that it's printing Ltac arguments. As a consequence, the arguments are not properly quoted (e.g. if they are tactic expressions, they are not within [ltac:(...)].
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions