diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-13 22:28:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-13 22:28:14 +0200 |
| commit | 3bb0753d1589489b0e33f6a116a84c4fa72ed49f (patch) | |
| tree | 02fce91ef79106ddf3fbd1eecb325bf081f5b7bb | |
| parent | 784d82dc1a709c4c262665a4cd4eb0b1bd1487a0 (diff) | |
Fix test-suite file, only part 2 is fixed in 8.5
| -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 ef79b9869..5ba0787ee 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 |