1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v
new file mode 100644
index 00000000..4300de16
--- /dev/null
+++ b/test-suite/bugs/closed/2590.v
@@ -0,0 +1,20 @@
+Require Import TestSuite.admit.
+Require Import Relation_Definitions RelationClasses Setoid SetoidClass.
+
+Section Bug.
+
+  Context {A : Type} (R : relation A).
+  Hypothesis pre : PreOrder R.
+  Context `{SA : Setoid A}.
+
+  Goal True.
+  set (SA' := SA).
+    assert ( forall SA0 : Setoid A,
+               @PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ).
+    rename SA into SA0.
+    intro SA.
+    admit.
+    admit.
+Qed.
+End Bug.
+