diff options
| author | Arnaud Spiwack | 2014-10-23 18:14:37 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | f5577e1ca7d7fa1424d0001377a3b2a10af7243b (patch) | |
| tree | fd9c648ddc18e09ee430244374373d3537e1aeea /stm/asyncTaskQueue.ml | |
| parent | f68208495d83c670039a95b6b44809b263e43ef2 (diff) | |
Info: print a name for the primitive tactics in [Proofview].
The name is chosen in accordance to Ltac's syntax. In particular [refine] prints as Ltac's refine, which is not entirely correct (Ltac's refine does some βι-reduction after refinement). Maybe it would be better to give make it clear that it is a different refine. Still in refine, the constr is printed without taking into account the new evars, which, apart from potentially getting the order of the goals wrong, prints new evars as ?x instead of ?[x]. A printer for terms with new evars will be necessary.
In the case of [V82.tactic], the name is just <unknown> because there is no way to retrieve any information. It won't appear in the first level of info in Ltac, however, if the user would require a deeper trace, he may see internal tactics (Tactics defined with TACTIC EXTEND also have weird, unparsable, internal names).
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions