diff options
| -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) ] ] ; |