3 files changed, 9 insertions, 15 deletions
diff --git a/theories/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v
index 29bd732c78..b4aed4c3f7 100644
--- a/theories/extraction/ExtrOcamlBigIntConv.v
+++ b/theories/extraction/ExtrOcamlBigIntConv.v
@@ -8,12 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Extraction to Ocaml: conversion from/to [big_int] *)
+(** Extraction to OCaml: conversion from/to [Z.t] *)
 
-(** 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). *)
+(** NB: The extracted code should be linked with [zarith.cm(x)a] and with
+    the [big.ml] wrapper. The latter can be found in the sources of Coq. *)
 
 Require Coq.extraction.Extraction.
 
diff --git a/theories/extraction/ExtrOcamlNatBigInt.v b/theories/extraction/ExtrOcamlNatBigInt.v
index 8a7ba92a94..c854f8fd5d 100644
--- a/theories/extraction/ExtrOcamlNatBigInt.v
+++ b/theories/extraction/ExtrOcamlNatBigInt.v
@@ -8,17 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Extraction of [nat] into Ocaml's [big_int] *)
+(** Extraction of [nat] into Zarith's [Z.t] *)
 
 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). *)
+(** NB: The extracted code should be linked with [zarith.cm(x)a] and with
+    the [big.ml] wrapper. The latter 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.
diff --git a/theories/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v
index 40a47b36fa..df9153a46d 100644
--- a/theories/extraction/ExtrOcamlZBigInt.v
+++ b/theories/extraction/ExtrOcamlZBigInt.v
@@ -8,17 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *)
+(** Extraction of [positive], [N], and [Z], into Zarith's [Z.t] *)
 
 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). *)
+(** NB: The extracted code should be linked with [zarith.cm(x)a] and with
+    the [big.ml] wrapper. The latter 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.