From eba0385132101d033db9ee8566fdd398a646d48b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 18 Jan 2006 14:26:35 +0000
Subject: Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas
 d'interférence avec des notations utilisateurs qui le remettrait mot-clé plus
 tard

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

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4f10bca748..3ecc2d4adf 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -281,7 +281,7 @@ GEXTEND Gram
     [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ]
   ;
   by_tactic:
-    [ [ "by"; tac = tactic -> tac | -> TacId "" ] ]
+    [ [ IDENT "by"; tac = tactic -> tac | -> TacId "" ] ]
   ;
   simple_tactic:
     [ [ 
-- 
cgit v1.2.3