diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_4816.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_4816.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_4816.v b/test-suite/bugs/closed/bug_4816.v index 00a523842e..50cb7d280a 100644 --- a/test-suite/bugs/closed/bug_4816.v +++ b/test-suite/bugs/closed/bug_4816.v @@ -1,3 +1,4 @@ +#[universes(polymorphic)] Section foo. Polymorphic Universes A B. Fail Constraint A <= B. @@ -5,12 +6,14 @@ End foo. (* gives an anomaly Universe undefined *) Universes X Y. +#[universes(polymorphic)] Section Foo. Polymorphic Universes Z W. Polymorphic Constraint W < Z. Fail Definition bla := Type@{W}. Polymorphic Definition bla := Type@{W}. + #[universes(polymorphic)] Section Bar. Fail Constraint X <= Z. End Bar. @@ -21,8 +24,10 @@ Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := { refl : forall x, r x x }. +#[universes(polymorphic)] Section qux. Polymorphic Universes A. + #[universes(polymorphic)] Section bar. Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. |