From d3b2c6f8a6864c44236b1f4b2ac89a025f49b7cd Mon Sep 17 00:00:00 2001
From: courtieu
Date: Mon, 1 Oct 2012 16:17:51 +0000
Subject: 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
---
 printing/pptactic.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'printing')

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
-- 
cgit v1.2.3