[build] Consolidate stdlib's .v files under a single directory.

Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003

21 files changed, 0 insertions, 1080 deletions

diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
deleted file mode 100644
index d08a81da64..0000000000
--- a/plugins/extraction/ExtrHaskellBasic.v
+++ /dev/null
@@ -1,17 +0,0 @@
-(** 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 => "()" [ "()" ].
-Extract Inductive list => "([])" [ "([])" "(:)" ].
-Extract Inductive prod => "(,)" [ "(,)" ].
-
-Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
-Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
-Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
-
-Extract Inlined Constant andb => "(Prelude.&&)".
-Extract Inlined Constant orb => "(Prelude.||)".
-Extract Inlined Constant negb => "Prelude.not".
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
deleted file mode 100644
index 267322d9ed..0000000000
--- a/plugins/extraction/ExtrHaskellNatInt.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(** Extraction of [nat] into Haskell's [Int] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Arith.
-Require Import ExtrHaskellNatNum.
-
-(**
- * Disclaimer: trying to obtain efficient certified programs
- * by extracting [nat] into [Int] is definitively *not* a good idea.
- * See comments in [ExtrOcamlNatInt.v].
- *)
-
-Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
-  "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v
deleted file mode 100644
index 4c5c71f58a..0000000000
--- a/plugins/extraction/ExtrHaskellNatInteger.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(** Extraction of [nat] into Haskell's [Integer] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Arith.
-Require Import ExtrHaskellNatNum.
-
-(**
- * Disclaimer: trying to obtain efficient certified programs
- * by extracting [nat] into [Integer] isn't necessarily a good idea.
- * See comments in [ExtrOcamlNatInt.v].
-*)
-
-Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ]
-  "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
deleted file mode 100644
index 09b0444614..0000000000
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ /dev/null
@@ -1,37 +0,0 @@
-(**
- * Efficient (but uncertified) extraction of usual [nat] functions
- * into equivalent versions in Haskell's Prelude that are defined
- * for any [Num] typeclass instances.  Useful in combination with
- * [Extract Inductive nat] that maps [nat] onto a Haskell type that
- * implements [Num].
- *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Arith.
-Require Import EqNat.
-
-Extract Inlined Constant Nat.add => "(Prelude.+)".
-Extract Inlined Constant Nat.mul => "(Prelude.*)".
-Extract Inlined Constant Nat.max => "Prelude.max".
-Extract Inlined Constant Nat.min => "Prelude.min".
-Extract Inlined Constant Init.Nat.add => "(Prelude.+)".
-Extract Inlined Constant Init.Nat.mul => "(Prelude.*)".
-Extract Inlined Constant Init.Nat.max => "Prelude.max".
-Extract Inlined Constant Init.Nat.min => "Prelude.min".
-Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
-Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
-Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
-Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
-Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
-Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
-
-Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
-Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
-Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
-Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
-
-Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
-Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
deleted file mode 100644
index 8c61f4e96b..0000000000
--- a/plugins/extraction/ExtrHaskellString.v
+++ /dev/null
@@ -1,62 +0,0 @@
-(**
- * Special handling of ascii and strings for extraction to Haskell.
- *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Ascii.
-Require Import String.
-Require Import Coq.Strings.Byte.
-
-(**
- * At the moment, Coq's extraction has no way to add extra import
- * statements to the extracted Haskell code.  You will have to
- * manually add:
- *
- *   import qualified Data.Bits
- *   import qualified Data.Char
- *)
-
-Extract Inductive ascii => "Prelude.Char"
-  [ "(\b0 b1 b2 b3 b4 b5 b6 b7 -> Data.Char.chr (
-      (if b0 then Data.Bits.shiftL 1 0 else 0) Prelude.+
-      (if b1 then Data.Bits.shiftL 1 1 else 0) Prelude.+
-      (if b2 then Data.Bits.shiftL 1 2 else 0) Prelude.+
-      (if b3 then Data.Bits.shiftL 1 3 else 0) Prelude.+
-      (if b4 then Data.Bits.shiftL 1 4 else 0) Prelude.+
-      (if b5 then Data.Bits.shiftL 1 5 else 0) Prelude.+
-      (if b6 then Data.Bits.shiftL 1 6 else 0) Prelude.+
-      (if b7 then Data.Bits.shiftL 1 7 else 0)))" ]
-  "(\f a -> f (Data.Bits.testBit (Data.Char.ord a) 0)
-              (Data.Bits.testBit (Data.Char.ord a) 1)
-              (Data.Bits.testBit (Data.Char.ord a) 2)
-              (Data.Bits.testBit (Data.Char.ord a) 3)
-              (Data.Bits.testBit (Data.Char.ord a) 4)
-              (Data.Bits.testBit (Data.Char.ord a) 5)
-              (Data.Bits.testBit (Data.Char.ord a) 6)
-              (Data.Bits.testBit (Data.Char.ord a) 7))".
-Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
-Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
-
-Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
-Extract Inlined Constant String.string_dec => "(Prelude.==)".
-Extract Inlined Constant String.eqb => "(Prelude.==)".
-
-(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
-Extract Inductive byte => "Prelude.Char"
-["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
-
-Extract Inlined Constant Byte.eqb => "(Prelude.==)".
-Extract Inlined Constant Byte.byte_eq_dec => "(Prelude.==)".
-Extract Inlined Constant Ascii.ascii_of_byte => "(\x -> x)".
-Extract Inlined Constant Ascii.byte_of_ascii => "(\x -> x)".
-
-(*
-Require Import ExtrHaskellBasic.
-Definition test := "ceci est un test"%string.
-Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)).
-Definition test3 := List.map ascii_of_nat (List.seq 0 256).
-
-Extraction Language Haskell.
-Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect.
-*)
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v
deleted file mode 100644
index 0345ffc4e8..0000000000
--- a/plugins/extraction/ExtrHaskellZInt.v
+++ /dev/null
@@ -1,26 +0,0 @@
-(** Extraction of [Z] into Haskell's [Int] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import ZArith.
-Require Import ExtrHaskellZNum.
-
-(**
- * Disclaimer: trying to obtain efficient certified programs
- * by extracting [Z] into [Int] is definitively *not* a good idea.
- * See comments in [ExtrOcamlNatInt.v].
- *)
-
-Extract Inductive positive => "Prelude.Int" [
-  "(\x -> 2 Prelude.* x Prelude.+ 1)"
-  "(\x -> 2 Prelude.* x)"
-  "1" ]
-  "(\fI fO fH n -> if n Prelude.== 1 then fH () else
-                   if Prelude.odd n
-                   then fI (n `Prelude.div` 2)
-                   else fO (n `Prelude.div` 2))".
-
-Extract Inductive Z => "Prelude.Int" [ "0" "(\x -> x)" "Prelude.negate" ]
-  "(\fO fP fN n -> if n Prelude.== 0 then fO () else
-                   if n Prelude.> 0 then fP n else
-                   fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v
deleted file mode 100644
index f7f9e2f80d..0000000000
--- a/plugins/extraction/ExtrHaskellZInteger.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(** Extraction of [Z] into Haskell's [Integer] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import ZArith.
-Require Import ExtrHaskellZNum.
-
-(** Disclaimer: trying to obtain efficient certified programs
-    by extracting [Z] into [Integer] isn't necessarily a good idea.
-    See comments in [ExtrOcamlNatInt.v].
-*)
-
-Extract Inductive positive => "Prelude.Integer" [
-  "(\x -> 2 Prelude.* x Prelude.+ 1)"
-  "(\x -> 2 Prelude.* x)"
-  "1" ]
-  "(\fI fO fH n -> if n Prelude.== 1 then fH () else
-                   if Prelude.odd n
-                   then fI (n `Prelude.div` 2)
-                   else fO (n `Prelude.div` 2))".
-
-Extract Inductive Z => "Prelude.Integer" [ "0" "(\x -> x)" "Prelude.negate" ]
-  "(\fO fP fN n -> if n Prelude.== 0 then fO () else
-                   if n Prelude.> 0 then fP n else
-                   fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
deleted file mode 100644
index 4141bd203f..0000000000
--- a/plugins/extraction/ExtrHaskellZNum.v
+++ /dev/null
@@ -1,23 +0,0 @@
-(**
- * Efficient (but uncertified) extraction of usual [Z] functions
- * into equivalent versions in Haskell's Prelude that are defined
- * for any [Num] typeclass instances.  Useful in combination with
- * [Extract Inductive Z] that maps [Z] onto a Haskell type that
- * implements [Num].
- *)
-
-Require Coq.extraction.Extraction.
-
-Require Import ZArith.
-Require Import EqNat.
-
-Extract Inlined Constant Z.add => "(Prelude.+)".
-Extract Inlined Constant Z.sub => "(Prelude.-)".
-Extract Inlined Constant Z.mul => "(Prelude.*)".
-Extract Inlined Constant Z.max => "Prelude.max".
-Extract Inlined Constant Z.min => "Prelude.min".
-Extract Inlined Constant Z_ge_lt_dec => "(Prelude.>=)".
-Extract Inlined Constant Z_gt_le_dec => "(Prelude.>)".
-
-Extract Constant Z.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Z.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/ExtrOCamlFloats.v b/plugins/extraction/ExtrOCamlFloats.v
deleted file mode 100644
index 1891772cc2..0000000000
--- a/plugins/extraction/ExtrOCamlFloats.v
+++ /dev/null
@@ -1,61 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction to OCaml of native binary64 floating-point numbers.
-
-Note: the extraction of primitive floats relies on Coq's internal file
-kernel/float64.ml, so make sure the corresponding binary is available
-when linking the extracted OCaml code.
-
-For example, if you build a (_CoqProject + coq_makefile)-based project
-and if you created an empty subfolder "extracted" and a file "test.v"
-containing [Cd "extracted". Separate Extraction function_to_extract.],
-you will just need to add in the _CoqProject: [test.v], [-I extracted]
-and the list of [extracted/*.ml] and [extracted/*.mli] files, then add
-[CAMLFLAGS += -w -33] in the Makefile.local file.  *)
-
-From Coq Require Floats Extraction.
-
-(** Basic data types used by some primitive operators. *)
-
-Extract Inductive bool => bool [ true false ].
-Extract Inductive prod => "( * )" [ "" ].
-
-Extract Inductive FloatClass.float_class =>
-  "Float64.float_class"
-  [ "PNormal" "NNormal" "PSubn" "NSubn" "PZero" "NZero" "PInf" "NInf" "NaN" ].
-Extract Inductive PrimFloat.float_comparison =>
-  "Float64.float_comparison"
-  [ "FEq" "FLt" "FGt" "FNotComparable" ].
-
-(** Primitive types and operators. *)
-
-Extract Constant PrimFloat.float => "Float64.t".
-Extraction Inline PrimFloat.float.
-(* Otherwise, the name conflicts with the primitive OCaml type [float] *)
-
-Extract Constant PrimFloat.classify => "Float64.classify".
-Extract Constant PrimFloat.abs => "Float64.abs".
-Extract Constant PrimFloat.sqrt => "Float64.sqrt".
-Extract Constant PrimFloat.opp => "Float64.opp".
-Extract Constant PrimFloat.eqb => "Float64.eq".
-Extract Constant PrimFloat.ltb => "Float64.lt".
-Extract Constant PrimFloat.leb => "Float64.le".
-Extract Constant PrimFloat.compare => "Float64.compare".
-Extract Constant PrimFloat.mul => "Float64.mul".
-Extract Constant PrimFloat.add => "Float64.add".
-Extract Constant PrimFloat.sub => "Float64.sub".
-Extract Constant PrimFloat.div => "Float64.div".
-Extract Constant PrimFloat.of_int63 => "Float64.of_int63".
-Extract Constant PrimFloat.normfr_mantissa => "Float64.normfr_mantissa".
-Extract Constant PrimFloat.frshiftexp => "Float64.frshiftexp".
-Extract Constant PrimFloat.ldshiftexp => "Float64.ldshiftexp".
-Extract Constant PrimFloat.next_up => "Float64.next_up".
-Extract Constant PrimFloat.next_down => "Float64.next_down".
diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v
deleted file mode 100644
index a2ee602313..0000000000
--- a/plugins/extraction/ExtrOCamlInt63.v
+++ /dev/null
@@ -1,56 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction to OCaml of native 63-bit machine integers. *)
-
-From Coq Require Int63 Extraction.
-
-(** Basic data types used by some primitive operators. *)
-
-Extract Inductive bool => bool [ true false ].
-Extract Inductive prod => "( * )" [ "" ].
-Extract Inductive comparison => int [ "0" "(-1)" "1" ].
-Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ].
-
-(** Primitive types and operators. *)
-Extract Constant Int63.int => "Uint63.t".
-Extraction Inline Int63.int.
-(* Otherwise, the name conflicts with the primitive OCaml type [int] *)
-
-Extract Constant Int63.lsl => "Uint63.l_sl".
-Extract Constant Int63.lsr => "Uint63.l_sr".
-Extract Constant Int63.land => "Uint63.l_and".
-Extract Constant Int63.lor => "Uint63.l_or".
-Extract Constant Int63.lxor => "Uint63.l_xor".
-
-Extract Constant Int63.add => "Uint63.add".
-Extract Constant Int63.sub => "Uint63.sub".
-Extract Constant Int63.mul => "Uint63.mul".
-Extract Constant Int63.mulc => "Uint63.mulc".
-Extract Constant Int63.div => "Uint63.div".
-Extract Constant Int63.mod => "Uint63.rem".
-
-Extract Constant Int63.eqb => "Uint63.equal".
-Extract Constant Int63.ltb => "Uint63.lt".
-Extract Constant Int63.leb => "Uint63.le".
-
-Extract Constant Int63.addc => "Uint63.addc".
-Extract Constant Int63.addcarryc => "Uint63.addcarryc".
-Extract Constant Int63.subc => "Uint63.subc".
-Extract Constant Int63.subcarryc => "Uint63.subcarryc".
-
-Extract Constant Int63.diveucl => "Uint63.diveucl".
-Extract Constant Int63.diveucl_21 => "Uint63.div21".
-Extract Constant Int63.addmuldiv => "Uint63.addmuldiv".
-
-Extract Constant Int63.compare => "Uint63.compare".
-
-Extract Constant Int63.head0 => "Uint63.head0".
-Extract Constant Int63.tail0 => "Uint63.tail0".
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
deleted file mode 100644
index 2f82b24862..0000000000
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Require Coq.extraction.Extraction.
-
-(** Extraction to Ocaml : use of basic Ocaml types *)
-
-Extract Inductive bool => bool [ true false ].
-Extract Inductive option => option [ Some None ].
-Extract Inductive unit => unit [ "()" ].
-Extract Inductive list => list [ "[]" "( :: )" ].
-Extract Inductive prod => "( * )" [ "" ].
-
-(** NB: The "" above is a hack, but produce nicer code than "(,)" *)
-
-(** Mapping sumbool to bool and sumor to option is not always nicer,
-    but it helps when realizing stuff like [lt_eq_lt_dec] *)
-
-Extract Inductive sumbool => bool [ true false ].
-Extract Inductive sumor => option [ Some None ].
-
-(** Restore laziness of andb, orb.
-    NB: without these Extract Constant, andb/orb would be inlined
-    by extraction in order to have laziness, producing inelegant
-    (if ... then ... else false) and (if ... then true else ...).
-*)
-
-Extract Inlined Constant andb => "(&&)".
-Extract Inlined Constant orb => "(||)".
-
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
deleted file mode 100644
index f8bc86d087..0000000000
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ /dev/null
@@ -1,112 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction to Ocaml: conversion from/to [big_int] *)
-
-(** NB: The extracted code should be linked with [nums.cm(x)a]
-    from ocaml's stdlib and with the wrapper [big.ml] that
-    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.
-Parameter bigint_zero : bigint.
-Parameter bigint_succ : bigint -> bigint.
-Parameter bigint_opp : bigint -> bigint.
-Parameter bigint_twice : bigint -> bigint.
-
-Extract Inlined Constant bigint => "Big.big_int".
-Extract Inlined Constant bigint_zero => "Big.zero".
-Extract Inlined Constant bigint_succ => "Big.succ".
-Extract Inlined Constant bigint_opp => "Big.opp".
-Extract Inlined Constant bigint_twice => "Big.double".
-
-Definition bigint_of_nat : nat -> bigint :=
- (fix loop acc n :=
-  match n with
-   | O => acc
-   | S n => loop (bigint_succ acc) n
-  end) bigint_zero.
-
-Fixpoint bigint_of_pos p :=
- match p with
-  | xH => bigint_succ bigint_zero
-  | xO p => bigint_twice (bigint_of_pos p)
-  | xI p => bigint_succ (bigint_twice (bigint_of_pos p))
- end.
-
-Fixpoint bigint_of_z z :=
- match z with
-  | Z0 => bigint_zero
-  | Zpos p => bigint_of_pos p
-  | Zneg p => bigint_opp (bigint_of_pos p)
- end.
-
-Fixpoint bigint_of_n n :=
- match n with
-  | N0 => bigint_zero
-  | Npos p => bigint_of_pos p
- end.
-
-(** NB: as for [pred] or [minus], [nat_of_bigint], [n_of_bigint] and
-    [pos_of_bigint] are total and return zero (resp. one) for
-    non-positive inputs. *)
-
-Parameter bigint_natlike_rec : forall A, A -> (A->A) -> bigint -> A.
-Extract Constant bigint_natlike_rec => "Big.nat_rec".
-
-Definition nat_of_bigint : bigint -> nat := bigint_natlike_rec _ O S.
-
-Parameter bigint_poslike_rec : forall A, (A->A) -> (A->A) -> A -> bigint -> A.
-Extract Constant bigint_poslike_rec => "Big.positive_rec".
-
-Definition pos_of_bigint : bigint -> positive := bigint_poslike_rec _ xI xO xH.
-
-Parameter bigint_zlike_case :
- forall A, A -> (bigint->A) -> (bigint->A) -> bigint -> A.
-Extract Constant bigint_zlike_case => "Big.z_rec".
-
-Definition z_of_bigint : bigint -> Z :=
- bigint_zlike_case _ Z0 (fun i => Zpos (pos_of_bigint i))
-                        (fun i => Zneg (pos_of_bigint i)).
-
-Definition n_of_bigint : bigint -> N :=
- bigint_zlike_case _ N0 (fun i => Npos (pos_of_bigint i)) (fun _ => N0).
-
-(* Tests:
-
-Definition small := 1234%nat.
-Definition big := 12345678901234567890%positive.
-
-Definition nat_0 := nat_of_bigint (bigint_of_nat 0).
-Definition nat_1 := nat_of_bigint (bigint_of_nat small).
-Definition pos_1 := pos_of_bigint (bigint_of_pos 1).
-Definition pos_2 := pos_of_bigint (bigint_of_pos big).
-Definition n_0 := n_of_bigint (bigint_of_n 0).
-Definition n_1 := n_of_bigint (bigint_of_n 1).
-Definition n_2 := n_of_bigint (bigint_of_n (Npos big)).
-Definition z_0 := z_of_bigint (bigint_of_z 0).
-Definition z_1 := z_of_bigint (bigint_of_z 1).
-Definition z_2 := z_of_bigint (bigint_of_z (Zpos big)).
-Definition z_m1 := z_of_bigint (bigint_of_z (-1)).
-Definition z_m2 := z_of_bigint (bigint_of_z (Zneg big)).
-
-Definition test :=
- (nat_0, nat_1, pos_1, pos_2, n_0, n_1, n_2, z_0, z_1, z_2, z_m1, z_m2).
-Definition check :=
- (O, small, xH, big, 0%N, 1%N, Npos big, 0%Z, 1%Z, Zpos big, (-1)%Z, Zneg big).
-
-Extraction "/tmp/test.ml" check test.
-
-... and we check that test=check
-*)
diff --git a/plugins/extraction/ExtrOcamlChar.v b/plugins/extraction/ExtrOcamlChar.v
deleted file mode 100644
index 1e68365dd3..0000000000
--- a/plugins/extraction/ExtrOcamlChar.v
+++ /dev/null
@@ -1,45 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Extraction to Ocaml : extract ascii to OCaml's char type *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Ascii String Coq.Strings.Byte.
-
-Extract Inductive ascii => char
-[
-"(* If this appears, you're using Ascii internals. Please don't *)
- (fun (b0,b1,b2,b3,b4,b5,b6,b7) ->
-  let f b i = if b then 1 lsl i else 0 in
-  Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))"
-]
-"(* If this appears, you're using Ascii internals. Please don't *)
- (fun f c ->
-  let n = Char.code c in
-  let h i = (n land (1 lsl i)) <> 0 in
-  f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))".
-
-Extract Constant zero => "'\000'".
-Extract Constant one => "'\001'".
-Extract Constant shift =>
- "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
-
-Extract Inlined Constant ascii_dec => "(=)".
-Extract Inlined Constant Ascii.eqb => "(=)".
-
-(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
-Extract Inductive byte => char
-["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
-
-Extract Inlined Constant Byte.eqb => "(=)".
-Extract Inlined Constant Byte.byte_eq_dec => "(=)".
-Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)".
-Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)".
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
deleted file mode 100644
index 2de1906323..0000000000
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ /dev/null
@@ -1,101 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction to Ocaml: conversion from/to [int]
-
-    Nota: no check that [int] values aren't generating overflows *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Arith ZArith.
-
-Parameter int : Type.
-Parameter int_zero : int.
-Parameter int_succ : int -> int.
-Parameter int_opp : int -> int.
-Parameter int_twice : int -> int.
-
-Extract Inlined Constant int => int.
-Extract Inlined Constant int_zero => "0".
-Extract Inlined Constant int_succ => "succ".
-Extract Inlined Constant int_opp => "-".
-Extract Inlined Constant int_twice => "2 *".
-
-Definition int_of_nat : nat -> int :=
- (fix loop acc n :=
-  match n with
-   | O => acc
-   | S n => loop (int_succ acc) n
-  end) int_zero.
-
-Fixpoint int_of_pos p :=
- match p with
-  | xH => int_succ int_zero
-  | xO p => int_twice (int_of_pos p)
-  | xI p => int_succ (int_twice (int_of_pos p))
- end.
-
-Fixpoint int_of_z z :=
- match z with
-  | Z0 => int_zero
-  | Zpos p => int_of_pos p
-  | Zneg p => int_opp (int_of_pos p)
- end.
-
-Fixpoint int_of_n n :=
- match n with
-  | N0 => int_zero
-  | Npos p => int_of_pos p
- end.
-
-(** NB: as for [pred] or [minus], [nat_of_int], [n_of_int] and
-    [pos_of_int] are total and return zero (resp. one) for
-    non-positive inputs. *)
-
-Parameter int_natlike_rec : forall A, A -> (A->A) -> int -> A.
-Extract Constant int_natlike_rec =>
-"fun fO fS ->
- let rec loop acc i = if i <= 0 then acc else loop (fS acc) (i-1)
- in loop fO".
-
-Definition nat_of_int : int -> nat := int_natlike_rec _ O S.
-
-Parameter int_poslike_rec : forall A, A -> (A->A) -> (A->A) -> int -> A.
-Extract Constant int_poslike_rec =>
-"fun f1 f2x f2x1 ->
- let rec loop i = if i <= 1 then f1 else
-  if i land 1 = 0 then f2x (loop (i lsr 1)) else f2x1 (loop (i lsr 1))
- in loop".
-
-Definition pos_of_int : int -> positive := int_poslike_rec _ xH xO xI.
-
-Parameter int_zlike_case : forall A, A -> (int->A) -> (int->A) -> int -> A.
-Extract Constant int_zlike_case =>
-"fun f0 fpos fneg i ->
- if i = 0 then f0 else if i>0 then fpos i else fneg (-i)".
-
-Definition z_of_int : int -> Z :=
- int_zlike_case _ Z0 (fun i => Zpos (pos_of_int i))
-                     (fun i => Zneg (pos_of_int i)).
-
-Definition n_of_int : int -> N :=
- int_zlike_case _ N0 (fun i => Npos (pos_of_int i)) (fun _ => N0).
-
-(** Warning: [z_of_int] is currently wrong for Ocaml's [min_int],
-    since [min_int] has no positive opposite ([-min_int = min_int]).
-*)
-
-(*
-Extraction "/tmp/test.ml"
-  nat_of_int int_of_nat
-  pos_of_int int_of_pos
-  z_of_int int_of_z
-  n_of_int int_of_n.
-*)
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
deleted file mode 100644
index a66d6e41fd..0000000000
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ /dev/null
@@ -1,73 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction of [nat] into Ocaml's [big_int] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Arith Even Div2 EqNat Euclid.
-Require Import ExtrOcamlBasic.
-
-(** NB: The extracted code should be linked with [nums.cm(x)a]
-    from ocaml's stdlib and with the wrapper [big.ml] that
-    simplifies the use of [Big_int] (it can be found in the sources
-    of Coq). *)
-
-(** Disclaimer: trying to obtain efficient certified programs
-    by extracting [nat] into [big_int] isn't necessarily a good idea.
-    See comments in [ExtrOcamlNatInt.v].
-*)
-
-
-(** Mapping of [nat] into [big_int]. The last string corresponds to
-    a [nat_case], see documentation of [Extract Inductive]. *)
-
-Extract Inductive nat => "Big.big_int" [ "Big.zero" "Big.succ" ]
- "Big.nat_case".
-
-(** Efficient (but uncertified) versions for usual [nat] functions *)
-
-Extract Constant plus => "Big.add".
-Extract Constant mult => "Big.mult".
-Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)".
-Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)".
-Extract Constant max => "Big.max".
-Extract Constant min => "Big.min".
-(*Extract Constant nat_beq => "Big.eq".*)
-Extract Constant EqNat.beq_nat => "Big.eq".
-Extract Constant EqNat.eq_nat_decide => "Big.eq".
-
-Extract Constant Peano_dec.eq_nat_dec => "Big.eq".
-
-Extract Constant Nat.compare =>
- "Big.compare_case Eq Lt Gt".
-
-Extract Constant Compare_dec.leb => "Big.le".
-Extract Constant Compare_dec.le_lt_dec => "Big.le".
-Extract Constant Compare_dec.lt_eq_lt_dec =>
- "Big.compare_case (Some false) (Some true) None".
-
-Extract Constant Even.even_odd_dec =>
- "fun n -> Big.sign (Big.mod n Big.two) = 0".
-Extract Constant Div2.div2 => "fun n -> Big.div n Big.two".
-
-Extract Inductive Euclid.diveucl => "(Big.big_int * Big.big_int)" [""].
-Extract Constant Euclid.eucl_dev => "fun n m -> Big.quomod m n".
-Extract Constant Euclid.quotient => "fun n m -> Big.div m n".
-Extract Constant Euclid.modulo => "fun n m -> Big.modulo m n".
-
-(*
-Require Import Euclid.
-Definition test n m (H:m>0) :=
- let (q,r,_,_) := eucl_dev m H n in
- nat_compare n (q*m+r).
-
-Extraction "/tmp/test.ml" test fact pred minus max min Div2.div2.
-*)
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
deleted file mode 100644
index 406a7f0d2b..0000000000
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ /dev/null
@@ -1,84 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction of [nat] into Ocaml's [int] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Arith Even Div2 EqNat Euclid.
-Require Import ExtrOcamlBasic.
-
-(** Disclaimer: trying to obtain efficient certified programs
-    by extracting [nat] into [int] is definitively *not* a good idea:
-
-    - This is just a syntactic adaptation, many things can go wrong,
-    such as name captures (e.g. if you have a constant named "int"
-    in your development, or a module named "Pervasives"). See bug #2878.
-
-    - Since [int] is bounded while [nat] is (theoretically) infinite,
-    you have to make sure by yourself that your program will not
-    manipulate numbers greater than [max_int]. Otherwise you should
-    consider the translation of [nat] into [big_int].
-
-    - Moreover, the mere translation of [nat] into [int] does not
-    change the complexity of functions. For instance, [mult] stays
-    quadratic. To mitigate this, we propose here a few efficient (but
-    uncertified) realizers for some common functions over [nat].
-
-    This file is hence provided mainly for testing / prototyping
-    purpose. For serious use of numbers in extracted programs,
-    you are advised to use either coq advanced representations
-    (positive, Z, N, BigN, BigZ) or modular/axiomatic representation.
-*)
-
-
-(** Mapping of [nat] into [int]. The last string corresponds to
-    a [nat_case], see documentation of [Extract Inductive]. *)
-
-Extract Inductive nat => int [ "0" "Pervasives.succ" ]
- "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
-
-(** Efficient (but uncertified) versions for usual [nat] functions *)
-
-Extract Constant plus => "(+)".
-Extract Constant pred => "fun n -> Pervasives.max 0 (n-1)".
-Extract Constant minus => "fun n m -> Pervasives.max 0 (n-m)".
-Extract Constant mult => "( * )".
-Extract Inlined Constant max => "Pervasives.max".
-Extract Inlined Constant min => "Pervasives.min".
-(*Extract Inlined Constant nat_beq => "(=)".*)
-Extract Inlined Constant EqNat.beq_nat => "(=)".
-Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
-
-Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)".
-
-Extract Constant Nat.compare =>
- "fun n m -> if n=m then Eq else if n<m then Lt else Gt".
-Extract Inlined Constant Compare_dec.leb => "(<=)".
-Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
-Extract Inlined Constant Compare_dec.lt_dec => "(<)".
-Extract Constant Compare_dec.lt_eq_lt_dec =>
- "fun n m -> if n>m then None else Some (n<m)".
-
-Extract Constant Even.even_odd_dec => "fun n -> n mod 2 = 0".
-Extract Constant Div2.div2 => "fun n -> n/2".
-
-Extract Inductive Euclid.diveucl => "(int * int)" [ "" ].
-Extract Constant Euclid.eucl_dev => "fun n m -> (m/n, m mod n)".
-Extract Constant Euclid.quotient => "fun n m -> m/n".
-Extract Constant Euclid.modulo => "fun n m -> m mod n".
-
-(*
-Definition test n m (H:m>0) :=
- let (q,r,_,_) := eucl_dev m H n in
- nat_compare n (q*m+r).
-
-Recursive Extraction test fact.
-*)
diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v
deleted file mode 100644
index ec3da1e444..0000000000
--- a/plugins/extraction/ExtrOcamlNativeString.v
+++ /dev/null
@@ -1,87 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Extraction to Ocaml : extract ascii to OCaml's char type
-   and string to OCaml's string type. *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Ascii String Coq.Strings.Byte.
-Require Export ExtrOcamlChar.
-
-(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
-Extract Inductive byte => char
-["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
-
-Extract Inlined Constant Byte.eqb => "(=)".
-Extract Inlined Constant Byte.byte_eq_dec => "(=)".
-Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)".
-Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)".
-
-(* This differs from ExtrOcamlString.v: the latter extracts "string"
-   to "char list", and we extract "string" to "string" *)
-
-Extract Inductive string => "string"
-[
-(* EmptyString *)
-"(* If this appears, you're using String internals. Please don't *)
-  """"
-"
-(* String *)
-"(* If this appears, you're using String internals. Please don't *)
-  (fun (c, s) -> String.make 1 c ^ s)
-"
-]
-"(* If this appears, you're using String internals. Please don't *)
- (fun f0 f1 s ->
-    let l = String.length s in
-    if l = 0 then f0 else f1 (String.get s 0) (String.sub s 1 (l-1)))
-".
-
-Extract Inlined Constant String.string_dec => "(=)".
-Extract Inlined Constant String.eqb => "(=)".
-Extract Inlined Constant String.append => "(^)".
-Extract Inlined Constant String.concat => "String.concat".
-Extract Inlined Constant String.prefix =>
-  "(fun s1 s2 ->
-     let l1 = String.length s1 and l2 = String.length s2 in
-     l1 <= l2 && String.sub s2 0 l1 = s1)".
-Extract Inlined Constant String.string_of_list_ascii =>
-  "(fun l ->
-      let a = Array.of_list l in
-      String.init (Array.length a) (fun i -> a.(i)))".
-Extract Inlined Constant String.list_ascii_of_string =>
-  "(fun s ->
-      Array.to_list (Array.init (String.length s) (fun i -> s.[i])))".
-Extract Inlined Constant String.string_of_list_byte =>
-  "(fun l ->
-      let a = Array.of_list l in
-      String.init (Array.length a) (fun i -> a.(i)))".
-Extract Inlined Constant String.list_byte_of_string =>
-  "(fun s ->
-      Array.to_list (Array.init (String.length s) (fun i -> s.[i])))".
-
-(* Other operations in module String (at the time of this writing):
-      String.length
-      String.get
-      String.substring
-      String.index
-      String.findex
-   They all use type "nat".  If we know that "nat" extracts
-   to O | S of nat, we can provide OCaml implementations
-   for these functions that work directly on OCaml's strings.
-   However "nat" could be extracted to other OCaml types...
-*)
-
-(*
-Definition test := "ceci est un test"%string.
-
-Recursive Extraction test Ascii.zero Ascii.one.
-*)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
deleted file mode 100644
index 18c5ed3fe4..0000000000
--- a/plugins/extraction/ExtrOcamlString.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Extraction to Ocaml : special handling of ascii and strings *)
-
-Require Coq.extraction.Extraction.
-
-Require Import Ascii String Coq.Strings.Byte.
-Require Export ExtrOcamlChar.
-
-Extract Inductive string => "char list" [ "[]" "(::)" ].
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
deleted file mode 100644
index c36ea50755..0000000000
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ /dev/null
@@ -1,91 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import ZArith NArith.
-Require Import ExtrOcamlBasic.
-
-(** NB: The extracted code should be linked with [nums.cm(x)a]
-    from ocaml's stdlib and with the wrapper [big.ml] that
-    simplifies the use of [Big_int] (it can be found in the sources
-    of Coq). *)
-
-(** Disclaimer: trying to obtain efficient certified programs
-    by extracting [Z] into [big_int] isn't necessarily a good idea.
-    See the Disclaimer in [ExtrOcamlNatInt]. *)
-
-(** Mapping of [positive], [Z], [N] into [big_int]. The last strings
-    emulate the matching, see documentation of [Extract Inductive]. *)
-
-Extract Inductive positive => "Big.big_int"
- [ "Big.doubleplusone" "Big.double" "Big.one" ] "Big.positive_case".
-
-Extract Inductive Z => "Big.big_int"
- [ "Big.zero" "" "Big.opp" ] "Big.z_case".
-
-Extract Inductive N => "Big.big_int"
- [ "Big.zero" "" ] "Big.n_case".
-
-(** Nota: the "" above is used as an identity function "(fun p->p)" *)
-
-(** Efficient (but uncertified) versions for usual functions *)
-
-Extract Constant Pos.add => "Big.add".
-Extract Constant Pos.succ => "Big.succ".
-Extract Constant Pos.pred => "fun n -> Big.max Big.one (Big.pred n)".
-Extract Constant Pos.sub => "fun n m -> Big.max Big.one (Big.sub n m)".
-Extract Constant Pos.mul => "Big.mult".
-Extract Constant Pos.min => "Big.min".
-Extract Constant Pos.max => "Big.max".
-Extract Constant Pos.compare =>
- "fun x y -> Big.compare_case Eq Lt Gt x y".
-Extract Constant Pos.compare_cont =>
- "fun c x y -> Big.compare_case c Lt Gt x y".
-
-Extract Constant N.add => "Big.add".
-Extract Constant N.succ => "Big.succ".
-Extract Constant N.pred => "fun n -> Big.max Big.zero (Big.pred n)".
-Extract Constant N.sub => "fun n m -> Big.max Big.zero (Big.sub n m)".
-Extract Constant N.mul => "Big.mult".
-Extract Constant N.min => "Big.min".
-Extract Constant N.max => "Big.max".
-Extract Constant N.div =>
- "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b".
-Extract Constant N.modulo =>
- "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b".
-Extract Constant N.compare => "Big.compare_case Eq Lt Gt".
-
-Extract Constant Z.add => "Big.add".
-Extract Constant Z.succ => "Big.succ".
-Extract Constant Z.pred => "Big.pred".
-Extract Constant Z.sub => "Big.sub".
-Extract Constant Z.mul => "Big.mult".
-Extract Constant Z.opp => "Big.opp".
-Extract Constant Z.abs => "Big.abs".
-Extract Constant Z.min => "Big.min".
-Extract Constant Z.max => "Big.max".
-Extract Constant Z.compare => "Big.compare_case Eq Lt Gt".
-
-Extract Constant Z.of_N => "fun p -> p".
-Extract Constant Z.abs_N => "Big.abs".
-
-(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
-    For the moment we don't even try *)
-
-(** Test:
-Require Import ZArith NArith.
-
-Extraction "/tmp/test.ml"
- Pos.add Pos.pred Pos.sub Pos.mul Pos.compare N.pred N.sub N.div N.modulo N.compare
- Z.add Z.mul Z.compare Z.of_N Z.abs_N Z.div Z.modulo.
-*)
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
deleted file mode 100644
index c7343d2468..0000000000
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ /dev/null
@@ -1,84 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Extraction of [positive], [N] and [Z] into Ocaml's [int] *)
-
-Require Coq.extraction.Extraction.
-
-Require Import ZArith NArith.
-Require Import ExtrOcamlBasic.
-
-(** Disclaimer: trying to obtain efficient certified programs
-    by extracting [Z] into [int] is definitively *not* a good idea.
-    See the Disclaimer in [ExtrOcamlNatInt]. *)
-
-(** Mapping of [positive], [Z], [N] into [int]. The last strings
-    emulate the matching, see documentation of [Extract Inductive]. *)
-
-Extract Inductive positive => int
-[ "(fun p->1+2*p)" "(fun p->2*p)" "1" ]
-"(fun f2p1 f2p f1 p ->
-  if p<=1 then f1 () else if p mod 2 = 0 then f2p (p/2) else f2p1 (p/2))".
-
-Extract Inductive Z => int [ "0" "" "(~-)" ]
-"(fun f0 fp fn z -> if z=0 then f0 () else if z>0 then fp z else fn (-z))".
-
-Extract Inductive N => int [ "0" "" ]
-"(fun f0 fp n -> if n=0 then f0 () else fp n)".
-
-(** Nota: the "" above is used as an identity function "(fun p->p)" *)
-
-(** Efficient (but uncertified) versions for usual functions *)
-
-Extract Constant Pos.add => "(+)".
-Extract Constant Pos.succ => "Pervasives.succ".
-Extract Constant Pos.pred => "fun n -> Pervasives.max 1 (n-1)".
-Extract Constant Pos.sub => "fun n m -> Pervasives.max 1 (n-m)".
-Extract Constant Pos.mul => "( * )".
-Extract Constant Pos.min => "Pervasives.min".
-Extract Constant Pos.max => "Pervasives.max".
-Extract Constant Pos.compare =>
- "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
-Extract Constant Pos.compare_cont =>
- "fun c x y -> if x=y then c else if x<y then Lt else Gt".
-
-
-Extract Constant N.add => "(+)".
-Extract Constant N.succ => "Pervasives.succ".
-Extract Constant N.pred => "fun n -> Pervasives.max 0 (n-1)".
-Extract Constant N.sub => "fun n m -> Pervasives.max 0 (n-m)".
-Extract Constant N.mul => "( * )".
-Extract Constant N.min => "Pervasives.min".
-Extract Constant N.max => "Pervasives.max".
-Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b".
-Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b".
-Extract Constant N.compare =>
- "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
-
-
-Extract Constant Z.add => "(+)".
-Extract Constant Z.succ => "Pervasives.succ".
-Extract Constant Z.pred => "Pervasives.pred".
-Extract Constant Z.sub => "(-)".
-Extract Constant Z.mul => "( * )".
-Extract Constant Z.opp => "(~-)".
-Extract Constant Z.abs => "Pervasives.abs".
-Extract Constant Z.min => "Pervasives.min".
-Extract Constant Z.max => "Pervasives.max".
-Extract Constant Z.compare =>
- "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
-
-Extract Constant Z.of_N => "fun p -> p".
-Extract Constant Z.abs_N => "Pervasives.abs".
-
-(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
-    For the moment we don't even try *)
-
-
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
deleted file mode 100644
index 207c95247e..0000000000
--- a/plugins/extraction/Extraction.v
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Declare ML Module "extraction_plugin".