13 files changed, 96 insertions, 24 deletions
diff --git a/doc/changelog/01-kernel/13853-delay-native.rst b/doc/changelog/01-kernel/13853-delay-native.rst
new file mode 100644
index 0000000000..59bf960a0f
--- /dev/null
+++ b/doc/changelog/01-kernel/13853-delay-native.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  Native-code libraries used by :tacn:`native_compute` are now delayed
+  until an actual call to the :tacn:`native_compute` machinery is
+  performed. This should make Coq more responsive on some systems
+  (`#13853 <https://github.com/coq/coq/pull/13853>`_, fixes `#13849
+  <https://github.com/coq/coq/issues/13849>`_, by Guillaume Melquiond).
diff --git a/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst
new file mode 100644
index 0000000000..cd1ac3a35a
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst
@@ -0,0 +1,19 @@
+- **Added:**
+  :opt:`Debug` to control debug messages, functioning similarly to the warning system
+  (`#13202 <https://github.com/coq/coq/pull/13202>`_,
+  by Maxime Dénès and Gaëtan Gilbert).
+  The following flags have been converted (such that ``Set Flag`` becomes ``Set Debug "flag"``):
+
+  - ``Debug Unification`` to ``unification``
+
+  - ``Debug HO Unification`` to ``ho-unification``
+
+  - ``Debug Tactic Unification`` to ``tactic-unification``
+
+  - ``Congruence Verbose`` to ``congruence``
+
+  - ``Debug Cbv`` to ``cbv``
+
+  - ``Debug RAKAM`` to ``RAKAM``
+
+  - ``Debug Ssreflect`` to ``ssreflect``
diff --git a/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst
new file mode 100644
index 0000000000..e48b772f01
--- /dev/null
+++ b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  `coqc` now enforces that at most a single `.v` file can be passed in
+  the command line. Support for multiple `.v` files in the form of
+  `coqc f1.v f2.v` didn't properly work in 8.13, tho it was accepted.
+  (`#13876 <https://github.com/coq/coq/pull/13876>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/10-standard-library/13080-ascii.rst b/doc/changelog/10-standard-library/13080-ascii.rst
new file mode 100644
index 0000000000..167002283e
--- /dev/null
+++ b/doc/changelog/10-standard-library/13080-ascii.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  ``leb`` and ``ltb`` functions for ``ascii``
+  (`#13080 <https://github.com/coq/coq/pull/13080>`_,
+  by Yishuai Li).
diff --git a/doc/changelog/10-standard-library/13559-primitive_integers.rst b/doc/changelog/10-standard-library/13559-primitive_integers.rst
new file mode 100644
index 0000000000..c3cad79bd2
--- /dev/null
+++ b/doc/changelog/10-standard-library/13559-primitive_integers.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Library for signed primitive integers, Sint63. The following operations were added to the kernel: division, remainder, comparison functions, and arithmetic shift right. Everything else works the same for signed and unsigned ints.
+  (`#13559 <https://github.com/coq/coq/pull/13559>`_,
+  fixes `#12109 <https://github.com/coq/coq/issues/12109>`_,
+  by Ana Borges, Guillaume Melquiond and Pierre Roux).
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
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index cbe526be68..27eb64a83b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -286,6 +286,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Cyclic/Int63/Cyclic63.v
     theories/Numbers/Cyclic/Int63/PrimInt63.v
     theories/Numbers/Cyclic/Int63/Int63.v
+    theories/Numbers/Cyclic/Int63/Sint63.v
     theories/Numbers/Cyclic/Int63/Ring63.v
     theories/Numbers/Cyclic/ZModulo/ZModulo.v
     </dd>