diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-06-12 17:47:51 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
| commit | d9e54d65cc808eab2908beb7a7a2c96005118ace (patch) | |
| tree | b214d227a3c5186dd512fb0f53064b4220ff2648 | |
| parent | f72a67569ec8cb9160d161699302b67919da5686 (diff) | |
Allow declaring universe binders with no constraints with @{|}
| -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. |