From 5ab437509f84d7f2175cdd55e801647699998983 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 15 Jul 2002 14:16:52 +0000
Subject: Pour assurer une compatibilite avec la 7.3

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2870 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_basevernac.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 4089f70049..b535f1e24a 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -203,7 +203,8 @@ GEXTEND Gram
    [ [ IDENT "Token"; s = STRING ->
        Pp.warning "Token declarations are now useless"; VernacNop
 
-     | "Grammar"; IDENT "tactic"; IDENT "simple_tactic"; ":=";
+     | "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
+        OPT [ ":"; IDENT "tactic" ]; ":=";
         OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> 
 	  VernacTacticGrammar tl
 
-- 
cgit v1.2.3