Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

2 files changed, 8 insertions, 5 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index ae66791b0c..105b0445fd 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1497,12 +1497,12 @@ Numeral notations
      for only non-negative integers, and the given numeral is negative.
 
 
-   .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).
+   .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).
 
      The parsing function given to the :cmd:`Numeral Notation`
      vernacular is not of the right type.
 
-   .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int).  Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).
+   .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int).  Instead of Decimal.int, the types Decimal.uint or Z or Int63.int could be used (you may need to require BinNums or Decimal or Int63 first).
 
      The printing function given to the :cmd:`Numeral Notation`
      vernacular is not of the right type.
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index c33df52038..7b21b67eea 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -259,7 +259,7 @@ through the <tt>Require Import</tt> command.</p>
     </dd>
 
     <dt> <b>&nbsp;&nbsp;Cyclic</b>:
-       Abstract and 31-bits-based cyclic arithmetic
+       Abstract and 63-bits-based cyclic arithmetic
     </dt>
     <dd>
     theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -268,11 +268,14 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Cyclic/Int31/Cyclic31.v
     theories/Numbers/Cyclic/Int31/Ring31.v
     theories/Numbers/Cyclic/Int31/Int31.v
+    theories/Numbers/Cyclic/Int63/Cyclic63.v
+    theories/Numbers/Cyclic/Int63/Int63.v
+    theories/Numbers/Cyclic/Int63/Ring63.v
     theories/Numbers/Cyclic/ZModulo/ZModulo.v
     </dd>
 
     <dt> <b>&nbsp;&nbsp;Natural</b>:
-       Abstract and 31-bits-words-based natural arithmetic
+       Abstract and 63-bits-words-based natural arithmetic
     </dt>
     <dd>
     theories/Numbers/Natural/Abstract/NAdd.v
@@ -300,7 +303,7 @@ through the <tt>Require Import</tt> command.</p>
     </dd>
 
     <dt> <b>&nbsp;&nbsp;Integer</b>:
-       Abstract and concrete (especially 31-bits-words-based) integer
+       Abstract and concrete (especially 63-bits-words-based) integer
        arithmetic
     </dt>
     <dd>