From acdaab2a8c2ccb63df364bb75de8a515b2cef484 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Nov 2019 10:00:01 +0100
Subject: docs(gallina-extensions.rst): Say more on float literals extraction

---
 doc/sphinx/language/gallina-extensions.rst | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 3f122f122b..54669534c7 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2500,12 +2500,19 @@ dedicated, efficient rules to reduce the applications of these primitive
 operations, using the floating-point processor operators that are assumed
 to comply with the IEEE 754 standard for floating-point arithmetic.
 
-These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to
-types and functions of a :g:`Float64` 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:`ExtrOCamlFloats`
+module can be used when extracting to OCaml: it maps the Coq primitives to types
+and functions of a :g:`Float64` 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 (of type :g:`Float64.t`) are extracted to literal OCaml
+values (of type :g:`float`) written in hexadecimal notation and
+wrapped into the :g:`Float64.of_float` constructor, e.g.:
+:g:`Float64.of_float (0x1p+0)`.
+
 Bidirectionality hints
 ----------------------
 
-- 
cgit v1.2.3