diff options
Diffstat (limited to 'theories/extraction/ExtrOcamlBigIntConv.v')
| -rw-r--r-- | theories/extraction/ExtrOcamlBigIntConv.v | 8 |
1 files changed, 3 insertions, 5 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. |