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
---
 parsing/g_ltac.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'parsing')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 51839ee880..bc2803ae5e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -61,6 +61,7 @@ GEXTEND Gram
       | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
+      | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
-- 
cgit v1.2.3