diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:28:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-25 14:18:35 +0100 |
| commit | f8e639f3b81ae142f5b529be1ad90210fc259375 (patch) | |
| tree | d73251d05312b34ba8f6e38387c3a07372603588 /test-suite/success/polymorphism.v | |
| parent | d071eac98b7812ac5c03004b438022900885d874 (diff) | |
Fix interpretation of global universes in univdecl constraints.
Also nicer error when the constraints are impossible.
Diffstat (limited to 'test-suite/success/polymorphism.v')
| -rw-r--r-- | test-suite/success/polymorphism.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index c09a60a4d..b3f9a4994 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -202,6 +202,10 @@ Module binders. exact Type@{i}. Qed. + Monomorphic Universe M. + Fail Definition with_mono@{u|} : Type@{M} := Type@{u}. + Definition with_mono@{u|u < M} : Type@{M} := Type@{u}. + End binders. Section cats. |