4 files changed, 56 insertions, 11 deletions
diff --git a/test-suite/bugs/closed/bug_12917.v b/test-suite/bugs/closed/bug_12917.v
new file mode 100644
index 0000000000..cd6b0766c6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12917.v
@@ -0,0 +1 @@
+Fail Derive Inversion bla with (le _ _).
diff --git a/test-suite/bugs/closed/bug_13059.v b/test-suite/bugs/closed/bug_13059.v
new file mode 100644
index 0000000000..2416e3ad13
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13059.v
@@ -0,0 +1,31 @@
+Set Uniform Inductive Parameters.
+Inductive test (X : Set) : Prop :=
+with test2 (X : Set) : X -> Prop :=
+ | C (x : X) : test2 x.
+
+Require Import List.
+Import ListNotations.
+
+Set Suggest Proof Using.
+Set Primitive Projections.
+
+
+Section Grammar.
+Variable A : Type.
+
+Record grammar : Type := Grammar {
+  gm_nonterm :> Type ;
+  gm_rules :> list (gm_nonterm * list (A + gm_nonterm)) ;
+}.
+
+Set Uniform Inductive Parameters.
+Inductive lang (gm : grammar) : gm -> list A -> Prop :=
+| lang_rule S ps ws : In (S, ps) gm -> lmatch ps ws -> lang S (concat ws)
+with lmatch (gm : grammar) : list (A + gm) -> list (list A) -> Prop :=
+| lmatch_nil : lmatch [] []
+| lmatch_consL ps ws a : lmatch ps ws -> lmatch (inl a :: ps) ([a] :: ws)
+| lmatch_consR ps ws S w :
+    lang S w -> lmatch ps ws -> lmatch (inr S :: ps) (w :: ws)
+.
+
+End Grammar.
diff --git a/test-suite/bugs/closed/bug_13109.v b/test-suite/bugs/closed/bug_13109.v
new file mode 100644
index 0000000000..76511a44c5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13109.v
@@ -0,0 +1,24 @@
+Require Import Coq.Program.Tactics.
+
+Set Universe Polymorphism.
+Obligation Tactic := idtac.
+
+Program Definition foo : Type := _.
+Program Definition bar : Type := _.
+Admit Obligations.
+(* Error: Anomaly "Uncaught exception AcyclicGraph.Make(Point).AlreadyDeclared."
+Please report at http://coq.inria.fr/bugs/.
+ *)
+Print foo.
+Print foo_obligation_1.
+Print bar.
+Print bar_obligation_1.
+
+Program Definition baz : Type := _.
+Admit Obligations of baz.
+Print baz.
+Print baz_obligation_1.
+
+Admit Obligations.
+
+Fail Admit Obligations of nobody.
diff --git a/test-suite/bugs/closed/bug_2928.v b/test-suite/bugs/closed/bug_2928.v
deleted file mode 100644
index 21e92ae20c..0000000000
--- a/test-suite/bugs/closed/bug_2928.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Class Equiv A := equiv: A -> A -> Prop.
-Infix "=" := equiv : type_scope.
-
-Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.
-
-Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.
-
-Class SemiLattice A op `{Equiv A} :=
-    { semilattice_sg :>> SemiGroup A op
-    ; redundant : Associative op
-    }.