2 files changed, 55 insertions, 0 deletions
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.