diff options
| author | Arnaud Spiwack | 2014-08-06 17:25:57 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | 2629f056d71e10eee93b78a0b26b2b3672bf69ff (patch) | |
| tree | 4aad44aed489b1685478dbd09aacc6a51886181b /stm/asyncTaskQueue.ml | |
| parent | 35e5ce5a4bcf288e5a8d2d07f0c411abe9099880 (diff) | |
Info: print the name of atomic tactics.
The printing uses the printer for interpreted tactics. It only works for tactics which are defined in the new style. There are still a few atomic tactics in tacinterp which are defined in [V82] style. Namely:
exact, apply, clear, rename, reduce, change, (mutual variant of) fix, (mutual variant of) cofix
These print placeholder names which are never reparsable and not as useful.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions