3 files changed, 36 insertions, 6 deletions
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index 4505fc4b4d..7211d00dd0 100644
--- a/doc/sphinx/language/core/primitive.rst
+++ b/doc/sphinx/language/core/primitive.rst
@@ -8,15 +8,20 @@ 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):
+(excerpt from the :g:`PrimInt63` 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:
+This type can be understood as representing either unsigned or signed integers,
+depending on which module is imported or, more generally, which scope is open.
+:g:`Int63` and :g:`int63_scope` refer to the unsigned version, while :g:`Sint63`
+and :g:`sint63_scope` refer to the signed one.
+
+The :g:`PrimInt63` module declares the available operators for this type.
+For instance, equality of two unsigned primitive integers can be determined using
+the :g:`Int63.eqb` function, declared and specified as follows:
 
 .. coqdoc::
 
@@ -25,7 +30,9 @@ declared and specified as follows:
 
    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.
+The complete set of such operators can be found in the :g:`PrimInt63` module.
+The specifications and notations are in the :g:`Int63` and :g:`Sint63`
+modules.
 
 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.
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index dcc60195ed..e7237cf7eb 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -248,7 +248,7 @@ right arrow, or ``\>=`` for a greater than or equal sign.
 
 A larger number of latex tokens are supported by default. The full list
 is available here:
-https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml
+https://github.com/coq/coq/blob/master/ide/coqide/default_bindings_src.ml
 
 Custom bindings may be added, as explained further on.
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 609884ce1d..03571ad680 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1741,6 +1741,12 @@ Number notations
          sorts, primitive integers, primitive floats, primitive arrays and type
          constants for primitive types) will be considered for printing.
 
+         .. note::
+            For example, :n:`@qualid__type` can be :n:`PrimInt63.int`,
+            in which case :n:`@qualid__print` takes :n:`PrimInt63.int_wrapper` as input
+            instead of :n:`PrimInt63.int`. See below for an
+            :ref:`example <example-number-notation-primitive-int>`.
+
       .. _number-string-via:
 
       :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]`
@@ -2066,6 +2072,23 @@ The following errors apply to both string and number notations:
 
       Check 3.
 
+.. _example-number-notation-primitive-int:
+
+.. example:: Number Notation for primitive integers
+
+   This shows the use of the primitive
+   integers :n:`PrimInt63.int` as :n:`@qualid__type`. It is the way
+   parsing and printing of primitive integers are actually implemented
+   in `PrimInt63.v`.
+
+   .. coqtop:: in reset
+
+      Require Import Int63.
+      Definition parser (x : pos_neg_int63) : option int :=
+        match x with Pos p => Some p | Neg _ => None end.
+      Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x).
+      Number Notation int parser printer : int63_scope.
+
 .. _example-number-notation-non-inductive:
 
 .. example:: Number Notation for a non inductive type