diff options
| author | coqbot-app[bot] | 2021-03-31 06:31:36 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-31 06:31:36 +0000 |
| commit | 6b5102bad5a75ede001908709f0b159127887667 (patch) | |
| tree | 0ff54db09d96d5a93f88025d32384f9a8834b1c2 | |
| parent | 4eb219067baa0f9ea806794d242de13c3a3a2826 (diff) | |
| parent | 58f35aad952c94744f232b622ab07ffb5d932a15 (diff) | |
Merge PR #14022: Replace mentions of Num by Zarith.
Reviewed-by: pi8027
| -rw-r--r-- | theories/extraction/ExtrOcamlBigIntConv.v | 8 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlNatBigInt.v | 8 | ||||
| -rw-r--r-- | theories/extraction/ExtrOcamlZBigInt.v | 8 |
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. |