From 003031beb002efa703a2f262f9501362d56da720 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 1 Mar 2018 14:03:20 +0100 Subject: CHANGES and tests for with Definition @{univs} --- test-suite/modules/WithDefUBinders.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/modules/WithDefUBinders.v (limited to 'test-suite/modules') 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. -- cgit v1.2.3