diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d42b5f622..6ef0b4fa8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1181,6 +1181,8 @@ GEXTEND Gram [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference | IDENT "bigint" -> ETBigint | IDENT "binder" -> ETBinder true + | IDENT "pattern" -> ETPattern 0 + | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern n | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; |