diff options
| author | Gaëtan Gilbert | 2017-06-12 17:47:51 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-09-19 10:28:03 +0200 |
| commit | d9e54d65cc808eab2908beb7a7a2c96005118ace (patch) | |
| tree | b214d227a3c5186dd512fb0f53064b4220ff2648 /parsing | |
| parent | f72a67569ec8cb9160d161699302b67919da5686 (diff) | |
Allow declaring universe binders with no constraints with @{|}
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d93c2563d7..59eb2b4d6c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -238,9 +238,9 @@ GEXTEND Gram univ_decl : [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ]; cs = [ "|"; l' = LIST0 univ_constraint SEP ","; - ext = [ "+" -> true | -> false ] -> (l',ext) - | -> ([], true) ]; - "}" -> + ext = [ "+" -> true | -> false ]; "}" -> (l',ext) + | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ] + -> { univdecl_instance = l; univdecl_extensible_instance = ext; univdecl_constraints = fst cs; |