Merge PR #926: test-suite uses Extraction TestCompile

7 files changed, 14 insertions, 8 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/4720.v b/test-suite/bugs/closed/4720.v
index 9265b60c1..704331e78 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 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.