aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-06 14:04:18 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-06 14:04:18 +0200
commit950edbf1a9ddc0419347d809d1f3bb125174ce10 (patch)
tree1ac69605c6a453fb741a2df13590d7014a8841b8 /test-suite
parent886ed2ee99e9ab9f0fc9aabac06a555d3beba19c (diff)
Add test for #8004.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/8004.v47
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.