diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-01 14:03:20 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-05 14:21:47 +0100 |
commit | 003031beb002efa703a2f262f9501362d56da720 (patch) | |
tree | f116421e3c81702dfda965282837a42a58c61f00 /test-suite/modules | |
parent | 88f3b5a441a3aaeb637d0b109544fbe71b7560dd (diff) |
CHANGES and tests for with Definition @{univs}
Diffstat (limited to 'test-suite/modules')
-rw-r--r-- | test-suite/modules/WithDefUBinders.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v new file mode 100644 index 000000000..e68345516 --- /dev/null +++ b/test-suite/modules/WithDefUBinders.v @@ -0,0 +1,15 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo@{u v|u < v} : Type@{v}. +End T. + +Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}. + Definition foo@{u v} := Type@{u} : Type@{v}. +End M. + +Fail Module M' : T with Definition foo := Type. + +(* Without the binder expression we have to do trickery to get the + universes in the right order. *) +Module M' : T with Definition foo := let t := Type in t. |