diff options
| author | Arnaud Spiwack | 2014-09-17 12:34:49 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | 9826a9f56b11125d6d0b540546f04dc12f845090 (patch) | |
| tree | f25622e49f8dc4bf02ad583757f20aa13f4bdf12 /stm/asyncTaskQueue.ml | |
| parent | 2629f056d71e10eee93b78a0b26b2b3672bf69ff (diff) | |
Info: Tactics coming from [TACTIC EXTEND] print their names.
Since PMP's intervention, the [TACTIC EXTEND] tactics are not uniform: some are syntax, and some are just an internal name for an Ltac definition. The latter kind prints an internal name. It may be better to avoid printing them in the trace altogether. But I haven't figured out how to detect that properly yet.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions