3 files changed, 62 insertions, 3 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index c1eab8a970..d1b95e6203 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -606,7 +606,10 @@ Finally, it gives the definition of the usual orderings ``le``,
   single: ge (term)
   single: gt (term)
 
-.. coqtop:: in
+.. This emits a notation already used warning but it won't be shown to
+   the user.
+
+.. coqtop:: in warn
 
   Inductive le (n:nat) : nat -> Prop :=
   | le_n : le n n
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 25f983ac1e..8b7e5c9a02 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1651,6 +1651,13 @@ Declaring Implicit Arguments
    To know which are the implicit arguments of an object, use the
    command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`).
 
+.. warn:: Argument number @num is a trailing implicit so must be maximal.
+
+   For instance in
+
+   .. coqtop:: all
+
+      Arguments prod _ [_].
 
 Automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2260,3 +2267,52 @@ expression as described in :ref:`ltac`.
 This construction is useful when one wants to define complicated terms
 using highly automated tactics without resorting to writing the proof-term
 by means of the interactive proof engine.
+
+.. _primitive-integers:
+
+Primitive Integers
+--------------------------------
+
+The language of terms features 63-bit machine integers as values. The type of
+such a value is *axiomatized*; it is declared through the following sentence
+(excerpt from the :g:`Int63` module):
+
+.. coqdoc::
+
+   Primitive int := #int63_type.
+
+This type is equipped with a few operators, that must be similarly declared.
+For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function,
+declared and specified as follows:
+
+.. coqdoc::
+
+   Primitive eqb := #int63_eq.
+   Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
+
+   Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j.
+
+The complete set of such operators can be obtained looking at the :g:`Int63` module.
+
+These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
+:g:`Print Assumptions` command, as in the following example.
+
+.. coqtop:: in reset
+
+   From Coq Require Import Int63.
+   Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63.
+   Proof. apply eqb_correct; vm_compute; reflexivity. Qed.
+
+.. coqtop:: all
+
+   Print Assumptions one_minus_one_is_zero.
+
+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
+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.
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 9ab3f905e6..9bd41d79b7 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1023,7 +1023,7 @@ Mutually defined inductive types
 
    .. coqtop:: in
 
-      Variables A B : Set.
+      Parameters A B : Set.
 
       Inductive tree : Set := node : A -> forest -> tree
 
@@ -1533,7 +1533,7 @@ the following attributes names are recognized:
 
 .. example::
 
-   .. coqtop:: all reset
+   .. coqtop:: all reset warn
 
         From Coq Require Program.
         #[program] Definition one : nat := S _.