From 3bb0753d1589489b0e33f6a116a84c4fa72ed49f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 13 Jun 2016 22:28:14 +0200
Subject: Fix test-suite file, only part 2 is fixed in 8.5

---
 test-suite/bugs/closed/4816.v | 9 +--------
 1 file changed, 1 insertion(+), 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
-- 
cgit v1.2.3