From 8e58adef25aa61f67a36a6f4be74489efa7184a6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 27 Mar 2003 15:32:13 +0000
Subject: MAJ des mots-clés, Definition, Theorem, ...

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

diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index fe7c17ad15..dc78f5faab 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -200,9 +200,9 @@ GEXTEND Gram
     [ [ tac = tactic_expr -> tac ] ]
   ;
   Vernac_.command: 
-    [ [ deftok; IDENT "Definition"; b = tacdef_body ->
+    [ [ deftok; "Definition"; b = tacdef_body ->
           VernacDeclareTacticDefinition (false, [b])
-      | IDENT "Recursive"; deftok; IDENT "Definition"; 
+      | IDENT "Recursive"; deftok; "Definition"; 
         l = LIST1 tacdef_body SEP "with" ->
           VernacDeclareTacticDefinition (true, l) ] ]
   ;
-- 
cgit v1.2.3