diff options
| author | Pierre-Marie Pédrot | 2018-09-28 15:32:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-28 15:32:04 +0200 |
| commit | f070a1f6eb99de1461d5a846a4f9ed47dafa79c6 (patch) | |
| tree | a8b2ac7b57539abfe3dffe4184cca3970301864a /test-suite | |
| parent | a0bdf071f8767aab18b24f19321041e18263d574 (diff) | |
| parent | 2566d45fcc05c1cd80ba2ac16ef342e7f145f01a (diff) | |
Merge PR #8479: Fix #8478: Undeclared universe anomaly with sections
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/8478.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/8478.v b/test-suite/bugs/closed/8478.v new file mode 100644 index 0000000000..8baaf8686a --- /dev/null +++ b/test-suite/bugs/closed/8478.v @@ -0,0 +1,11 @@ +Set Universe Polymorphism. +Set Printing Universes. +Unset Strict Universe Declaration. + +Monomorphic Universe v. + +Section Foo. + Let bar := Type@{u}. + Fail Monomorphic Constraint bar.u < v. + +End Foo. (* was anomaly undeclared universe due to the constraint *) |