Merge PR #8008: Add test for #8004.

1 files changed, 47 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/8004.v b/test-suite/bugs/closed/8004.v
new file mode 100644
index 000000000..818639997
--- /dev/null
+++ b/test-suite/bugs/closed/8004.v
@@ -0,0 +1,47 @@
+Require Export Coq.Program.Tactics Coq.Classes.SetoidTactics Coq.Classes.CMorphisms .
+
+Set Universe Polymorphism.
+
+Delimit Scope category_theory_scope with category_theory.
+Open Scope category_theory_scope.
+
+Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.
+
+Class Setoid A := {
+  equiv : crelation A;
+  setoid_equiv :> Equivalence equiv
+}.
+
+Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.
+
+Open Scope list_scope.
+
+Generalizable All Variables.
+
+Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type :=
+  match xs, ys with
+  | nil, nil => True
+  | x :: xs, y :: ys => x ≈ y ∧ list_equiv xs ys
+  | _, _ => False
+  end.
+
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+
+Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv.
+Next Obligation.
+  repeat intro.
+  induction x; simpl; split; auto.
+  reflexivity.
+Qed.
+Next Obligation.
+  repeat intro.
+  generalize dependent y.
+  induction x, y; simpl; intros; auto.
+  destruct X; split.
+    now symmetry.
+  intuition.
+Qed.
+Next Obligation.
+admit.
+Defined.