diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 5baa23b3e9..0dea4fcc43 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram ; match_key: [ [ "match" -> { Once } - | "lazymatch" -> { Select } - | "multimatch" -> { General } ] ] + | IDENT "lazymatch" -> { Select } + | IDENT "multimatch" -> { General } ] ] ; input_fun: [ [ "_" -> { Name.Anonymous } |