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
---
 grammar/q_coqast.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3fd4600587..aae1d9de2a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -449,6 +449,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >>
   | Tacexpr.TacProgress t ->
       <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
+  | Tacexpr.TacShowHyps t ->
+      <:expr< Tacexpr.TacShowHyps $mlexpr_of_tactic t$ >>
   | Tacexpr.TacId l ->
       <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >>
   | Tacexpr.TacFail (n,l) ->
-- 
cgit v1.2.3