Imported Upstream version 8.6upstream/8.6

1 files changed, 37 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v
new file mode 100644
index 00000000..f54d6433
--- /dev/null
+++ b/test-suite/bugs/closed/4503.v
@@ -0,0 +1,37 @@
+Require Coq.Classes.RelationClasses.
+
+Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
+{ refl : forall x, r x x }.
+
+(* FAILURE 1 *)
+
+Section foo.
+  Polymorphic Universes A.
+  Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
+
+  Fail Definition foo := PO.
+End foo.
+
+
+Module ILogic.
+
+Set Universe Polymorphism.
+
+(* Logical connectives *)
+Class ILogic@{L} (A : Type@{L}) : Type := mkILogic
+{
+  lentails: A -> A -> Prop;
+  lentailsPre:> RelationClasses.PreOrder lentails
+}.
+
+
+End ILogic.
+
+Set Printing Universes.
+
+(* There is stil a problem if the class is universe polymorphic *)
+Section Embed_ILogic_Pre.
+  Polymorphic Universes A T.
+  Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
+
+End Embed_ILogic_Pre.
\ No newline at end of file