4 files changed, 96 insertions, 36 deletions
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 4a509da89..0ee223250 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 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)*)