diff options
| -rw-r--r-- | parsing/g_decl_mode.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index f37d1e758..e73e54e7f 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -54,8 +54,8 @@ GLOBAL: proof_instr; ]; justification_items : [[ -> Some [] - | IDENT "by"; l=LIST1 constr SEP "," -> Some l - | IDENT "by"; "*" -> None ]] + | "by"; l=LIST1 constr SEP "," -> Some l + | "by"; "*" -> None ]] ; justification_method : [[ -> None |