diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 070fc44775..acf68e9fd2 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2446,12 +2446,10 @@ operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Uint63` module (excepted :g:`addc`, :g:`addcarryc`, -:g:`subc`, :g:`subcarryc`, and :g:`diveucl` whose implementation in OCaml is -left to the reader). Said OCaml module is not produced by extraction. Instead, -it has to be provided by the user (if they want to compile or execute the -extracted code). For instance, an implementation of this module can be taken -from the kernel of Coq. +and functions of a :g:`Uint63` module. Said OCaml module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on |