16 files changed, 159 insertions, 44 deletions

diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v
index 098a7e9e72..c556ff0b2b 100644
--- a/test-suite/bugs/closed/2141.v
+++ b/test-suite/bugs/closed/2141.v
@@ -11,5 +11,6 @@ End FSetHide.
 
 Module NatSet' := FSetHide NatSet.
 Recursive Extraction NatSet'.fold.
+Extraction TestCompile NatSet'.fold.
 
 (* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v
index 1b758acd73..4b3e7ff054 100644
--- a/test-suite/bugs/closed/3287.v
+++ b/test-suite/bugs/closed/3287.v
@@ -6,6 +6,7 @@ Definition bar := true.
 End Foo.
 
 Recursive Extraction Foo.bar.
+Extraction TestCompile Foo.bar.
 
 Module Foo'.
 Definition foo := (I,I).
@@ -13,10 +14,6 @@ Definition bar := true.
 End Foo'.
 
 Recursive Extraction Foo'.bar.
+Extraction TestCompile Foo'.bar.
 
-Module Foo''.
-Definition foo := (I,I).
-Definition bar := true.
-End Foo''.
-
-Extraction Foo.bar.
+Extraction Foo'.bar.
diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
index 2fb0a5439a..1d9488c6e1 100644
--- a/test-suite/bugs/closed/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -33,3 +33,4 @@ Axiom empty_fieldstore : cert_fieldstore.
 End MkCertRuntimeTypes.
 
 Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)
+Extraction TestCompile MkCertRuntimeTypes.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
index a59975dbcf..d6660e3553 100644
--- a/test-suite/bugs/closed/4616.v
+++ b/test-suite/bugs/closed/4616.v
@@ -2,5 +2,6 @@ Require Coq.extraction.Extraction.
 
 Set Primitive Projections.
 Record Foo' := Foo { foo : Type }.
-Axiom f : forall t : Foo', foo t.
+Definition f := forall t : Foo', foo t.
 Extraction f.
+Extraction TestCompile f.
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/4710.v b/test-suite/bugs/closed/4710.v
index 5d8ca330ac..e792a36234 100644
--- a/test-suite/bugs/closed/4710.v
+++ b/test-suite/bugs/closed/4710.v
@@ -4,7 +4,6 @@ Set Primitive Projections.
 Record Foo' := Foo { foo : nat }.
 Extraction foo.
 Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
-Extraction Language Ocaml.
 Extraction foo2p.
 
 Definition bla (x : Foo2 0) := foo2p _ x.
@@ -12,3 +11,5 @@ Extraction bla.
 
 Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
 Extraction bla'.
+
+Extraction TestCompile foo foo2p bla bla'.
diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v
index 9265b60c17..704331e784 100644
--- a/test-suite/bugs/closed/4720.v
+++ b/test-suite/bugs/closed/4720.v
@@ -44,3 +44,7 @@ Recursive Extraction WithMod.
 Recursive Extraction WithDef.
 
 Recursive Extraction WithModPriv.
+
+(* Let's even check that all this extracted code is actually compilable: *)
+
+Extraction TestCompile WithMod WithDef WithModPriv.
diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v
index 231d103a59..7c8af1e46e 100644
--- a/test-suite/bugs/closed/5177.v
+++ b/test-suite/bugs/closed/5177.v
@@ -19,3 +19,4 @@ End MakeA.
 
 Require Extraction.
 Recursive Extraction MakeA.
+Extraction TestCompile MakeA.
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
diff --git a/test-suite/bugs/closed/5671.v b/test-suite/bugs/closed/5671.v
new file mode 100644
index 0000000000..c9a085045a
--- /dev/null
+++ b/test-suite/bugs/closed/5671.v
@@ -0,0 +1,7 @@
+(* Fixing Meta-unclean specialize *)
+
+Require Import Setoid.
+Axiom a : forall x, x=0 -> True.
+Lemma lem (x y1 y2:nat) (H:x=0) (H0:eq y1 y2) : y1 = y2.
+specialize a with (1:=H). clear H x. intros _.
+setoid_rewrite H0.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index ffea0819a5..a9ae74fd67 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -109,3 +109,9 @@ fun x : ?A => x === x
      : forall x : ?A, x = x
 where
 ?A : [x : ?A |- Type] (x cannot be used)
+{0, 1}
+     : nat * nat
+{0, 1, 2}
+     : nat * (nat * nat)
+{0, 1, 2, 3}
+     : nat * (nat * (nat * nat))
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 250aecafd4..dee0f70f79 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -160,3 +160,11 @@ End Bug4765.
 
 Notation "x === x" := (eq_refl x) (only printing, at level 10).
 Check (fun x => eq_refl x).
+
+(**********************************************************************)
+(* Test recursive notations with the recursive pattern repeated on the right *)
+
+Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..).
+Check {0,1}.
+Check {0,1,2}.
+Check {0,1,2,3}.
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 4a509da89e..0ee2232502 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -545,47 +545,96 @@ Recursive Extraction test_proj.
 
 (*** TO SUM UP: ***)
 
-(* Was previously producing a "test_extraction.ml" *)
-Recursive Extraction
-  idnat id id' test2 test3 test4 test5 test6 test7 d d2
-  d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
-  test13 test19 test20 nat sumbool_rect c Finite tree
-  tree_size test14 test15 eta_c test16 test17 test18 bidon
-  tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
-  tp1bis Truc oups test24 loop horibilis PropSet natbool
-  zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
-  f_arity f_normal Boite boite1 boite2 test_boite Box box1
-  zarb test_proj.
+Module Everything.
+ Definition idnat := idnat.
+ Definition id := id.
+ Definition id' := id'.
+ Definition test2 := test2.
+ Definition test3 := test3.
+ Definition test4 := test4.
+ Definition test5 := test5.
+ Definition test6 := test6.
+ Definition test7 := test7.
+ Definition d := d.
+ Definition d2 := d2.
+ Definition d3 := d3.
+ Definition d4 := d4.
+ Definition d5 := d5.
+ Definition d6 := d6.
+ Definition test8 := test8.
+ Definition test9 := test9.
+ Definition test10 := test10.
+ Definition test11 := test11.
+ Definition test12 := test12.
+ Definition test13 := test13.
+ Definition test19 := test19.
+ Definition test20 := test20.
+ Definition nat := nat.
+ Definition sumbool_rect := sumbool_rect.
+ Definition c := c.
+ Definition Finite := Finite.
+ Definition tree := tree.
+ Definition tree_size := tree_size.
+ Definition test14 := test14.
+ Definition test15 := test15.
+ Definition eta_c := eta_c.
+ Definition test16 := test16.
+ Definition test17 := test17.
+ Definition test18 := test18.
+ Definition bidon := bidon.
+ Definition tb := tb.
+ Definition fbidon := fbidon.
+ Definition fbidon2 := fbidon2.
+ Definition test_0 := test_0.
+ Definition test_1 := test_1.
+ Definition eq_rect := eq_rect.
+ Definition tp1 := tp1.
+ Definition tp1bis := tp1bis.
+ Definition Truc := Truc.
+ Definition oups := oups.
+ Definition test24 := test24.
+ Definition loop := loop.
+ Definition horibilis := horibilis.
+ Definition PropSet := PropSet.
+ Definition natbool := natbool.
+ Definition zerotrue := zerotrue.
+ Definition zeroTrue := zeroTrue.
+ Definition zeroprop := zeroprop.
+ Definition test21 := test21.
+ Definition test22 := test22.
+ Definition test23 := test23.
+ Definition f := f.
+ Definition f_prop := f_prop.
+ Definition f_arity := f_arity.
+ Definition f_normal := f_normal.
+ Definition Boite := Boite.
+ Definition boite1 := boite1.
+ Definition boite2 := boite2.
+ Definition test_boite := test_boite.
+ Definition Box := Box.
+ Definition box1 := box1.
+ Definition zarb := zarb.
+ Definition test_proj := test_proj.
+End Everything.
+
+(* Extraction "test_extraction.ml" Everything. *)
+Recursive Extraction Everything.
+(* Check that the previous OCaml code is compilable *)
+Extraction TestCompile Everything.
 
 Extraction Language Haskell.
-(* Was previously producing a "Test_extraction.hs" *)
-Recursive Extraction
- idnat id id' test2 test3 test4 test5 test6 test7 d d2
- d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
- test13 test19 test20 nat sumbool_rect c Finite tree
- tree_size test14 test15 eta_c test16 test17 test18 bidon
- tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
- tp1bis Truc oups test24 loop horibilis PropSet natbool
- zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
- f_arity f_normal Boite boite1 boite2 test_boite Box box1
- zarb test_proj.
+(* Extraction "Test_extraction.hs" Everything. *)
+Recursive Extraction Everything.
 
 Extraction Language Scheme.
-(* Was previously producing a "test_extraction.scm" *)
-Recursive Extraction
- idnat id id' test2 test3 test4 test5 test6 test7 d d2
- d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
- test13 test19 test20 nat sumbool_rect c Finite tree
- tree_size test14 test15 eta_c test16 test17 test18 bidon
- tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
- tp1bis Truc oups test24 loop horibilis PropSet natbool
- zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
- f_arity f_normal Boite boite1 boite2 test_boite Box box1
- zarb test_proj.
+(* Extraction "test_extraction.scm" Everything. *)
+Recursive Extraction Everything.
 
 
 (*** Finally, a test more focused on everyday's life situations ***)
 
 Require Import ZArith.
 
-Recursive Extraction two_or_two_plus_one Zdiv_eucl_exist.
+Extraction Language Ocaml.
+Recursive Extraction Z_modulo_2 Zdiv_eucl_exist.
+Extraction TestCompile Z_modulo_2 Zdiv_eucl_exist.
diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
index e770cf779a..fb0adabae9 100644
--- a/test-suite/success/extraction_dep.v
+++ b/test-suite/success/extraction_dep.v
@@ -4,7 +4,7 @@
 Require Coq.extraction.Extraction.
 
 (** NB: we should someday check the produced code instead of
-    simply running the commands. *)
+    extracting and just compiling. *)
 
 (** 1) Without signature ... *)
 
@@ -20,6 +20,7 @@ End A.
 Definition testA := A.u + A.B.x.
 
 Recursive Extraction testA. (* without: v w *)
+Extraction TestCompile testA.
 
 (** 1b) Same with an Include *)
 
@@ -31,6 +32,7 @@ End Abis.
 Definition testAbis := Abis.u + Abis.y.
 
 Recursive Extraction testAbis. (* without: A B v w x *)
+Extraction TestCompile testAbis.
 
 (** 2) With signature, we only keep elements mentionned in signature. *)
 
@@ -46,3 +48,4 @@ End Ater.
 Definition testAter := Ater.u.
 
 Recursive Extraction testAter. (* with only: u v *)
+Extraction TestCompile testAter.
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
index 5bf807b1c6..a38a688fb4 100644
--- a/test-suite/success/extraction_impl.v
+++ b/test-suite/success/extraction_impl.v
@@ -2,7 +2,7 @@
 (** Examples of extraction with manually-declared implicit arguments *)
 
 (** NB: we should someday check the produced code instead of
-    simply running the commands. *)
+    extracting and just compiling. *)
 
 Require Coq.extraction.Extraction.
 
@@ -22,9 +22,11 @@ Proof.
 Defined.
 
 Recursive Extraction dnat_nat.
+Extraction TestCompile dnat_nat.
 
 Extraction Implicit dnat_nat [n].
 Recursive Extraction dnat_nat.
+Extraction TestCompile dnat_nat.
 
 (** Same, with a Fixpoint *)
 
@@ -35,9 +37,11 @@ Fixpoint dnat_nat' n (d:dnat n) :=
  end.
 
 Recursive Extraction dnat_nat'.
+Extraction TestCompile dnat_nat'.
 
 Extraction Implicit dnat_nat' [n].
 Recursive Extraction dnat_nat'.
+Extraction TestCompile dnat_nat'.
 
 (** Bug #4243, part 2 *)
 
@@ -56,6 +60,7 @@ Defined.
 Extraction Implicit es [n].
 Extraction Implicit enat_nat [n].
 Recursive Extraction enat_nat.
+Extraction TestCompile enat_nat.
 
 (** Same, with a Fixpoint *)
 
@@ -67,6 +72,7 @@ Fixpoint enat_nat' n (e:enat n) : nat :=
 
 Extraction Implicit enat_nat' [n].
 Recursive Extraction enat_nat'.
+Extraction TestCompile enat_nat'.
 
 (** Bug #4228 *)
 
@@ -82,3 +88,4 @@ Extraction Implicit two_course [n].
 End Food.
 
 Recursive Extraction Food.Meal.
+Extraction TestCompile Food.Meal.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 789854b2d6..576bdbf71b 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -184,6 +184,7 @@ Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
 
 Require Coq.extraction.Extraction.
 Recursive Extraction term term'.
+Extraction TestCompile term term'.
 (*Unset Printing Primitive Projection Parameters.*)
 
 (* Primitive projections in the presence of let-ins (was not failing in beta3)*)