From 58f35aad952c94744f232b622ab07ffb5d932a15 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 28 Mar 2021 17:12:49 +0200
Subject: Replace mentions of Num by Zarith.

The documentation of extraction became outdated when the big.ml wrapper
got modified by 094e4649c29e2426daca0476c140439de901dafe.
---
 theories/extraction/ExtrOcamlBigIntConv.v | 8 +++-----
 theories/extraction/ExtrOcamlNatBigInt.v  | 8 +++-----
 theories/extraction/ExtrOcamlZBigInt.v    | 8 +++-----
 3 files changed, 9 insertions(+), 15 deletions(-)

(limited to 'theories')

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.
-- 
cgit v1.2.3