aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/ExtrHaskellBasic.v2
-rw-r--r--plugins/extraction/ExtrHaskellNatInt.v2
-rw-r--r--plugins/extraction/ExtrHaskellNatInteger.v2
-rw-r--r--plugins/extraction/ExtrHaskellNatNum.v2
-rw-r--r--plugins/extraction/ExtrHaskellString.v2
-rw-r--r--plugins/extraction/ExtrHaskellZInt.v2
-rw-r--r--plugins/extraction/ExtrHaskellZInteger.v2
-rw-r--r--plugins/extraction/ExtrHaskellZNum.v2
-rw-r--r--plugins/extraction/ExtrOcamlBasic.v2
-rw-r--r--plugins/extraction/ExtrOcamlBigIntConv.v2
-rw-r--r--plugins/extraction/ExtrOcamlIntConv.v2
-rw-r--r--plugins/extraction/ExtrOcamlNatBigInt.v2
-rw-r--r--plugins/extraction/ExtrOcamlNatInt.v2
-rw-r--r--plugins/extraction/ExtrOcamlString.v2
-rw-r--r--plugins/extraction/ExtrOcamlZBigInt.v2
-rw-r--r--plugins/extraction/ExtrOcamlZInt.v2
-rw-r--r--plugins/extraction/Extraction.v9
-rw-r--r--plugins/funind/FunInd.v10
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/micromega/MExtraction.v1
20 files changed, 53 insertions, 1 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
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
new file mode 100644
index 0000000000..e40aea7764
--- /dev/null
+++ b/plugins/funind/FunInd.v
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+Require Coq.extraction.Extraction.
+Declare ML Module "recdef_plugin".
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index e4433247b4..c6fcd647ff 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -6,8 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+Require Import Coq.funind.FunInd.
Require Import PeanoNat.
-
Require Compare_dec.
Require Wf_nat.
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 135a715203..95f135c8f0 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -14,6 +14,7 @@
(* Used to generate micromega.ml *)
+Require Extraction.
Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:05:02 +0000