2 files changed, 32 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12947.v b/test-suite/bugs/closed/bug_12947.v
new file mode 100644
index 0000000000..baf0579465
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12947.v
@@ -0,0 +1,9 @@
+Require Import BinPos Int63 PArray.
+
+Definition foo (n : positive) :=
+  let a := make 2 0 in
+  let b := Pos.iter (fun b => set b 1 1) a 100000 in
+  let v := get b 0 in
+  Pos.iter (fun v => v + get a 0) v n.
+
+Timeout 5 Time Eval vm_compute in foo 1000000.
diff --git a/test-suite/bugs/closed/bug_13117.v b/test-suite/bugs/closed/bug_13117.v
new file mode 100644
index 0000000000..5db3f9fadc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13117.v
@@ -0,0 +1,23 @@
+
+Class A := {}.
+
+Class B (x:A) := {}.
+Class B' (a:=A) (x:a) := {}.
+
+Fail Definition foo a `{B a} := 0.
+Definition foo a `{B' a} := 0.
+
+Record C (x:A) := {}.
+Existing Class C.
+
+Fail Definition bar a `{C a} := 0.
+
+
+Definition X := Type.
+
+Class Y (x:X) := {}.
+
+Definition before `{Y Set} := 0.
+
+Existing Class X.
+Fail Definition after `{Y Set} := 0.