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 /printing/printer.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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 75cce2755a..1880d90ee9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -51,6 +51,7 @@ let pr_lconstr_core goal_concl_style env sigma t = let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env +let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env let pr_lconstr_goal_style_env env = pr_lconstr_core true env let pr_constr_goal_style_env env = pr_constr_core true env |