3 files changed, 15 insertions, 7 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b722b1af74..9362a7729e 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -3,10 +3,6 @@
 Ltac2
 =====
 
-.. coqtop:: none
-
-   From Ltac2 Require Import Ltac2.
-
 The Ltac tactic language is probably one of the ingredients of the success of
 Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
 
@@ -88,6 +84,12 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML
 with unspecified effects would do, e.g. function reduction is substitution
 by a value.
 
+To import Ltac2, use the following command:
+
+.. coqtop:: in
+
+   From Ltac2 Require Import Ltac2.
+
 Type Syntax
 ~~~~~~~~~~~
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 853ddfd6dc..46215f16a6 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2222,14 +2222,14 @@ tactics to *permute* the subgoals generated by a tactic.
 
       If :token:`num`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
-      in focus. The first subgoal becomes :math:`G_{n + 1 − k}` and the
+      in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the
       circular order of subgoals remains unchanged.
 
    .. tacn:: first @num last
 
       If :token:`num`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
-      in focus. The first subgoal becomes :math:`G_k` and the circular order
+      in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order
       of subgoals remains unchanged.
 
 Finally, the tactics ``last`` and ``first`` combine with the branching syntax
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 53cfb973d4..2fa4f1fa42 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -275,7 +275,7 @@ These patterns can be used when the hypothesis is an equality:
    :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`),
    while :n:`and` has a single constructor (:n:`conj`) with multiple parameters
    (:n:`A` and :n:`B`).
-   These are defined in theories/Init/Logic.v.  The "where" clauses define the
+   These are defined in ``theories/Init/Logic.v``.  The "where" clauses define the
    infix notation for "or" and "and".
 
    .. coqdoc::
@@ -3113,6 +3113,12 @@ the conversion in hypotheses :n:`{+ @ident}`.
    compilation cost is higher, so it is worth using only for intensive
    computations.
 
+   .. flag:: NativeCompute Timing
+
+      This flag causes all calls to the native compiler to print
+      timing information for the compilation, execution, and
+      reification phases of native compilation.
+
    .. flag:: NativeCompute Profiling
 
       On Linux, if you have the ``perf`` profiler installed, this flag makes