diff options
| author | courtieu | 2012-10-01 16:17:51 +0000 |
|---|---|---|
| committer | courtieu | 2012-10-01 16:17:51 +0000 |
| commit | d3b2c6f8a6864c44236b1f4b2ac89a025f49b7cd (patch) | |
| tree | 94985eacc1c3b416b9707802a4d2d2f8a5e8d5f9 /printing/pptactic.ml | |
| parent | 4a10b5e505df255a7ff8efa68214a14f50c24576 (diff) | |
Added a new tactical infoH tac, that displays the names of hypothesis created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c317d4f3f9..8bdea1356b 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -906,6 +906,9 @@ let rec pr_tac inherited tac = | TacProgress t -> hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t), ltactical + | TacShowHyps t -> + hov 1 (str "infoH" ++ spc () ++ spc () ++ pr_tac (ltactical,E) t), + ltactical | TacInfo t -> hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t), linfo |