diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -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 d93c2563d..59eb2b4d6 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; |