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

6 files changed, 10 insertions, 8 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/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/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.