diff options
| author | herbelin | 2003-03-27 15:32:13 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-27 15:32:13 +0000 |
| commit | 8e58adef25aa61f67a36a6f4be74489efa7184a6 (patch) | |
| tree | b6c114e5dfec547278ca5d6c2e6a2965b5c00ad8 | |
| parent | e603873cfd09399e1bae1154a2b710da6a82b33a (diff) | |
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
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 4 |
1 files 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) ] ] ; |