From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 test-suite/success/extraction.v | 128 ++++++++++++++++++++++++++++------------
 1 file changed, 90 insertions(+), 38 deletions(-)

(limited to 'test-suite/success/extraction.v')

diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0086e090..95ae0709 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,11 +1,14 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+Require Coq.extraction.Extraction.
 Require Import Arith.
 Require Import List.
 
@@ -544,47 +547,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.
-- 
cgit v1.2.3