From 8675b9d1a574aceb9a9d40c9c135db9c042e00b1 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 22 Jul 2019 12:47:53 +0000
Subject: [Int63] Implement all primitives in OCaml

Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are
implemented in the kernel so that they can be used by OCaml code (e.g.,
extracted code) as the other primitives.
---
 doc/sphinx/language/gallina-extensions.rst | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3