2 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4709.v b/test-suite/bugs/closed/4709.v
new file mode 100644
index 0000000000..a9edcc8043
--- /dev/null
+++ b/test-suite/bugs/closed/4709.v
@@ -0,0 +1,18 @@
+
+(** Bug 4709 https://coq.inria.fr/bug/4709
+    Extraction wasn't reducing primitive projections in types. *)
+
+Require Extraction.
+
+Set Primitive Projections.
+
+Record t := Foo { foo : Type }.
+Definition ty := foo (Foo nat).
+
+(* Without proper reduction of primitive projections in
+   [extract_type], the type [ty] was extracted as [Tunknown].
+   Let's check it isn't the case anymore. *)
+
+Parameter check : nat.
+Extract Constant check => "(O:ty)".
+Extraction TestCompile ty check.
diff --git a/test-suite/bugs/closed/5315.v b/test-suite/bugs/closed/5315.v
new file mode 100644
index 0000000000..f1f1b8c051
--- /dev/null
+++ b/test-suite/bugs/closed/5315.v
@@ -0,0 +1,10 @@
+Require Import Recdef.
+
+Function dumb_works (a:nat) {struct a} :=
+  match (fun x => x) a with O => O | S n' => dumb_works n' end.
+
+Function dumb_nope (a:nat) {struct a} :=
+  match (id (fun x => x)) a with O => O | S n' => dumb_nope n' end.
+
+(* This check is just present to ensure Function worked well *)
+Check R_dumb_nope_complete. 
+\ No newline at end of file