Merge PR #10430: [Extraction] Add support for primitive integers

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

3 files changed, 15 insertions, 2 deletions

diff --git a/doc/changelog/08-tools/10430-extraction-int63.rst b/doc/changelog/08-tools/10430-extraction-int63.rst
new file mode 100644
index 0000000000..68ae4591a4
--- /dev/null
+++ b/doc/changelog/08-tools/10430-extraction-int63.rst
@@ -0,0 +1,5 @@
+- Fix extraction to OCaml of primitive machine integers;
+  see :ref:`primitive-integers`
+  (`#10430 <https://github.com/coq/coq/pull/10430>`_,
+  fixes `#10361 <https://github.com/coq/coq/issues/10361>`_,
+  by Vincent Laporte).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index c93984661e..acf68e9fd2 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2443,12 +2443,19 @@ The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement
 dedicated, efficient, rules to reduce the applications of these primitive
 operations.
 
-These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to
-types and functions of a :g:`Uint63` module. Said module is not produced by
+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. 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
+64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the
+function :g:`Uint63.compile` from the kernel).
+
 Bidirectionality hints
 ----------------------
 
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index b25104ddb9..46175e37ed 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v
 plugins/extraction/ExtrHaskellZNum.v
 plugins/extraction/ExtrOcamlBasic.v
 plugins/extraction/ExtrOcamlBigIntConv.v
+plugins/extraction/ExtrOCamlInt63.v
 plugins/extraction/ExtrOcamlIntConv.v
 plugins/extraction/ExtrOcamlNatBigInt.v
 plugins/extraction/ExtrOcamlNatInt.v