diff options
| author | herbelin | 2003-03-27 15:24:08 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-27 15:24:08 +0000 |
| commit | e603873cfd09399e1bae1154a2b710da6a82b33a (patch) | |
| tree | 1ed816d15c5d7211f25370579112cb545dd30fa6 | |
| parent | 2db7c503a14ed44f6e18ffc02d9a2f3f5c4760e7 (diff) | |
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
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 20 |
1 files 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" -> () ] ] |