diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-25 17:09:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
| commit | 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (patch) | |
| tree | 77c1c1fdc54a7c96d197c71caa2ab75fc3041928 /parsing | |
| parent | 69822345c198aa6bf51354f6b84c7fd5d401bc9c (diff) | |
Notations: A step in cleaning constr_entry_key.
- Avoid dummy use of unit
- Do not decide as early as parsing the default level for pattern
- Prepare to further extensions
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6ef0b4fa8..009c1c19a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1181,8 +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 "pattern" -> ETPattern None + | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (Some n) | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; |