7 files changed, 55 insertions, 24 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/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 665bae7077..071fcbee11 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -675,10 +675,10 @@ Applying theorems
       :tacn:`notypeclasses refine`: it performs type checking without resolution of
       typeclasses, does not perform beta reductions or shelve the subgoals.
 
-   .. flag:: Debug Unification
-
-      Enables printing traces of unification steps used during
-      elaboration/typechecking and the :tacn:`refine` tactic.
+   :opt:`Debug` ``"unification"`` enables printing traces of
+   unification steps used during elaboration/typechecking and the
+   :tacn:`refine` tactic. ``"ho-unification"`` prints information
+   about higher order heuristics.
 
 .. tacn:: apply @term
    :name: apply
@@ -1040,10 +1040,9 @@ Applying theorems
       when the instantiation of a variable cannot be found
       (cf. :tacn:`eapply` and :tacn:`apply`).
 
-.. flag:: Debug Tactic Unification
-
-   Enables printing traces of unification steps in tactic unification.
-   Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`.
+:opt:`Debug` ``"tactic-unification"`` enables printing traces of
+unification steps in tactic unification. Tactic unification is used in
+tactics such as :tacn:`apply` and :tacn:`rewrite`.
 
 .. _managingthelocalcontext:
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 8db16fff69..37d605360d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -865,6 +865,14 @@ Controlling display
    interpreted from left to right, so in case of an overlap, the flags on the
    right have higher priority, meaning that `A,-A` is equivalent to `-A`.
 
+.. opt:: Debug "{+, {? - } @ident }"
+
+   Configures the display of debug messages. Each :n:`@ident` enables debug messages
+   for that component, while  :n:`-@ident` disables messages for the component.
+   ``all`` activates or deactivates all other components.  ``backtrace`` controls printing of
+   error backtraces.
+
+   :cmd:`Test` `Debug` displays the list of components and their enabled/disabled state.
 .. opt:: Printing Width @natural
 
    This command sets which left-aligned part of the width of the screen is used
diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst
index 5aaded2726..3f1f5d46c5 100644
--- a/doc/sphinx/proofs/automatic-tactics/logic.rst
+++ b/doc/sphinx/proofs/automatic-tactics/logic.rst
@@ -194,9 +194,7 @@ Solvers for logic and equality
       additional arguments can be given to congruence by filling in the holes in the
       terms given in the error message, using the `with` clause.
 
-   .. flag:: Congruence Verbose
-
-      Makes :tacn:`congruence` print debug information.
+   :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information.
 
 .. tacn:: btauto
 
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index bfaf746a06..4f937ad727 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -559,9 +559,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
       on the profile file to see the results. Consult the ``perf`` documentation
       for more details.
 
-.. flag:: Debug Cbv
-
-   This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
+   :opt:`Debug` ``"Cbv"`` makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
    information about the constants it encounters and the unfolding decisions it
    makes.
 
@@ -659,10 +657,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
 
-.. flag:: Debug RAKAM
-
-   This flag makes :tacn:`cbn` print various debugging information.
-   ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
+:opt:`Debug` ``"RAKAM"`` makes :tacn:`cbn` print various debugging information.
+``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
 
 .. tacn:: unfold @qualid
    :name: unfold
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