diff options
Diffstat (limited to 'test-suite/modules/WithDefUBinders.v')
-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 00000000..e6834551 --- /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. |