diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 2 |
2 files changed, 5 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; diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 0bd8bfe60..488443de1 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -159,6 +159,8 @@ End structures. Module binders. + Definition mynat@{|} := nat. + Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}. exact A. Defined. |