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

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

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 0b6e344a9b..8830001119 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -106,9 +106,9 @@ GEXTEND Gram
       | OPT[IDENT "Mutual"]; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
           VernacInductive (f,indl)
-      | IDENT "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+      | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint recs
-      | IDENT "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
+      | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
           VernacCoFixpoint corecs
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
   ;
@@ -124,23 +124,23 @@ GEXTEND Gram
     ] ]
   ;
   thm_token:
-    [ [ IDENT "Theorem" -> Theorem
+    [ [ "Theorem" -> Theorem
       | IDENT "Lemma" -> Lemma
       | IDENT "Fact" -> Fact
       | IDENT "Remark" -> Remark ] ]
   ;
   def_token:
-    [ [ IDENT "Definition" -> (fun _ _ -> ()), Global, GDefinition
+    [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition
       | IDENT "Local" -> (fun _ _ -> ()), Local, LDefinition
       | IDENT "SubClass"  -> Class.add_subclass_hook, Global, GCoercion
       | IDENT "Local"; IDENT "SubClass"  ->
           Class.add_subclass_hook, Local, LCoercion ] ] 
   ;
   assumption_token:
-    [ [ IDENT "Hypothesis" -> (Local, Logical)
-      | IDENT "Variable" -> (Local, Definitional)
-      | IDENT "Axiom" -> (Global, Logical)
-      | IDENT "Parameter" -> (Global, Definitional) ] ]
+    [ [ "Hypothesis" -> (Local, Logical)
+      | "Variable" -> (Local, Definitional)
+      | "Axiom" -> (Global, Logical)
+      | "Parameter" -> (Global, Definitional) ] ]
   ;
   assumptions_token:
     [ [ IDENT "Hypotheses" -> (Local, Logical)
@@ -148,8 +148,8 @@ GEXTEND Gram
       | IDENT "Parameters" -> (Global, Definitional) ] ]
   ;
   finite_token:
-    [ [ IDENT "Inductive" -> true
-      | IDENT "CoInductive" -> false ] ]
+    [ [ "Inductive" -> true
+      | "CoInductive" -> false ] ]
   ;
   record_token:
     [ [ IDENT "Record" -> () | IDENT "Structure" -> () ] ]
-- 
cgit v1.2.3