Merge remote-tracking branch 'upstream/trunk' into trunk

17 files changed, 41 insertions, 0 deletions

diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
index 294d61023b..d08a81da64 100644
--- a/plugins/extraction/ExtrHaskellBasic.v
+++ b/plugins/extraction/ExtrHaskellBasic.v
@@ -1,5 +1,7 @@
 (** Extraction to Haskell : use of basic Haskell types *)
 
+Require Coq.extraction.Extraction.
+
 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
 Extract Inductive unit => "()" [ "()" ].
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
index e94e7d42bd..267322d9ed 100644
--- a/plugins/extraction/ExtrHaskellNatInt.v
+++ b/plugins/extraction/ExtrHaskellNatInt.v
@@ -1,5 +1,7 @@
 (** Extraction of [nat] into Haskell's [Int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import ExtrHaskellNatNum.
 
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v
index 038f0ed817..4c5c71f58a 100644
--- a/plugins/extraction/ExtrHaskellNatInteger.v
+++ b/plugins/extraction/ExtrHaskellNatInteger.v
@@ -1,5 +1,7 @@
 (** Extraction of [nat] into Haskell's [Integer] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import ExtrHaskellNatNum.
 
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index 244eb85fc2..fabe9a4c67 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -6,6 +6,8 @@
  * implements [Num].
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import EqNat.
 
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index 3558f4f254..ac1f6f9130 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -2,6 +2,8 @@
  * Special handling of ascii and strings for extraction to Haskell.
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Ascii.
 Require Import String.
 
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v
index 66690851a7..0345ffc4e8 100644
--- a/plugins/extraction/ExtrHaskellZInt.v
+++ b/plugins/extraction/ExtrHaskellZInt.v
@@ -1,5 +1,7 @@
 (** Extraction of [Z] into Haskell's [Int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import ExtrHaskellZNum.
 
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v
index f192f16ee8..f7f9e2f80d 100644
--- a/plugins/extraction/ExtrHaskellZInteger.v
+++ b/plugins/extraction/ExtrHaskellZInteger.v
@@ -1,5 +1,7 @@
 (** Extraction of [Z] into Haskell's [Integer] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import ExtrHaskellZNum.
 
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
index cbbfda75e5..4141bd203f 100644
--- a/plugins/extraction/ExtrHaskellZNum.v
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -6,6 +6,8 @@
  * implements [Num].
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import EqNat.
 
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index d9b000c2af..dfdc498638 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+Require Coq.extraction.Extraction.
+
 (** Extraction to Ocaml : use of basic Ocaml types *)
 
 Extract Inductive bool => bool [ true false ].
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index c42938c8ec..78ee460856 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -13,6 +13,8 @@
     simplifies the use of [Big_int] (it can be found in the sources
     of Coq). *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith ZArith.
 
 Parameter bigint : Type.
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index 515fa52dfa..fcfea352a7 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -10,6 +10,8 @@
 
     Nota: no check that [int] values aren't generating overflows *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith ZArith.
 
 Parameter int : Type.
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 3149e70298..e0837be621 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [nat] into Ocaml's [big_int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 7c607f7ae6..80da72d43f 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [nat] into Ocaml's [int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 6af591eed3..64ca6c85d0 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -8,6 +8,8 @@
 
 (* Extraction to Ocaml : special handling of ascii and strings *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Ascii String.
 
 Extract Inductive ascii => char
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index c9e8eac0c5..66f188c84e 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 4d33174b35..c93cfb9d46 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -8,6 +8,8 @@
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
new file mode 100644
index 0000000000..ab1416b1d6
--- /dev/null
+++ b/plugins/extraction/Extraction.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Declare ML Module "extraction_plugin".
\ No newline at end of file