From aef53771eb41a891d5808432f78ccdec156445c0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 23 Mar 2001 23:25:31 +0000
Subject: Les règles d'affichage ajoutés dans le commit précédent avait le même
 nom que la règle pour command

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

(limited to 'syntax')

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index 19ec907910..2ee107c1bf 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -349,6 +349,6 @@ Syntax tactic
 
   level 8:
     tactic_to_constr [<<(COMMAND $c)>>] -> [ $c:"constr":9 ]
-  | tactic_to_constr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ]
-  | tactic_to_constr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ].
+  | tactic_to_castedconstr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ]
+  | tactic_to_openconstr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ].
 
-- 
cgit v1.2.3