test-suite: more use of the new command Extraction TestCompile

3 files changed, 13 insertions, 2 deletions

diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
index e770cf779..fb0adabae 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 5bf807b1c..a38a688fb 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 789854b2d..576bdbf71 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)*)