From e9eada02ae154c5b1cb0413a670fd4c81f0265eb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Mar 2001 17:52:56 +0000
Subject: Règle de syntaxe pour CASTEDCOMMAND

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1478 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 syntax/PPTactic.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'syntax')

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index a84a81f6ea..19ec907910 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -348,4 +348,7 @@ Syntax tactic
   ;
 
   level 8:
-  tactic_to_constr [<<(COMMAND $c)>>] -> [ $c:"constr":9 ].
+    tactic_to_constr [<<(COMMAND $c)>>] -> [ $c:"constr":9 ]
+  | tactic_to_constr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ]
+  | tactic_to_constr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ].
+
-- 
cgit v1.2.3