From 950cd6f7d123977ac0dffb27b0695b4eac52aa25 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Aug 2003 13:24:43 +0000
Subject: Pb de mot-cle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4272 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tacticnew.ml4 | 2 +-
 parsing/g_vernacnew.ml4 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 017cfd18f0..54c671ed69 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -213,7 +213,7 @@ GEXTEND Gram
   ;
   hypident:
     [ [ id = id_or_meta -> InHyp id
-      | "("; "type"; "of"; id = id_or_meta; ")" -> InHypType id ] ]
+      | "("; IDENT "type"; "of"; id = id_or_meta; ")" -> InHypType id ] ]
   ;
   clause:
     [ [ "in"; idl = LIST1 hypident -> idl
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index a9866b7e8b..02812d6de0 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -367,7 +367,7 @@ GEXTEND Gram
       ] ]
   ;
   with_declaration:
-    [ [ IDENT "Definition"; id = base_ident; ":="; c = Constr.constr ->
+    [ [ "Definition"; id = base_ident; ":="; c = Constr.constr ->
           CWith_Definition (id,c)
       | IDENT "Module"; id = base_ident; ":="; qid = qualid ->
 	  CWith_Module (id,qid)
-- 
cgit v1.2.3