diff options
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index e18769f5a3..aee1e7e00a 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -123,7 +123,7 @@ GEXTEND Gram | "()" -> TacVoid ] ] ; match_key: - [ [ b = [ IDENT "lazy" -> true | -> false ]; "match" -> b ] ] + [ [ "match" -> false ] ] ; input_fun: [ [ "_" -> None |