diff options
| -rw-r--r-- | test-suite/bugs/closed/4816.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v index ef79b9869b..5ba0787ee7 100644 --- a/test-suite/bugs/closed/4816.v +++ b/test-suite/bugs/closed/4816.v @@ -1,10 +1,3 @@ -Section foo. -Polymorphic Universes A B. -Constraint A <= B. -End foo. -(* gives an anomaly Universe undefined *) - -or even, a refinement of #4503: Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := @@ -13,6 +6,6 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type := Section foo. Polymorphic Universes A. Section bar. - Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. End foo.
\ No newline at end of file |