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

9 files changed, 23 insertions, 10 deletions

diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v
index 098a7e9e7..c556ff0b2 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 1b758acd7..4b3e7ff05 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 2fb0a5439..1d9488c6e 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 a59975dbc..d6660e355 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/4710.v b/test-suite/bugs/closed/4710.v
index 5d8ca330a..e792a3623 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/5177.v b/test-suite/bugs/closed/5177.v
index 231d103a5..7c8af1e46 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/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)*)