Convert rewriting and proof-mode chapters to prodn

5 files changed, 95 insertions, 158 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 87a367fc93..8b627c29a4 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -284,6 +284,8 @@ A sequence is an expression of the following form:
 .. tacn:: @ltac_expr3__1 ; {| @ltac_expr3__2 | @binder_tactic }
    :name: ltac-seq
 
+   .. todo: can't use "… ; …" as the name because of the semicolon
+
    The expression :n:`@ltac_expr3__1` is evaluated to :n:`v__1`, which must be
    a tactic value. The tactic :n:`v__1` is applied to the current goals,
    possibly producing more goals. Then the right-hand side is evaluated to
@@ -481,7 +483,6 @@ Do loop
 ~~~~~~~
 
 .. tacn:: do @nat_or_var @ltac_expr3
-   :name: do
 
    The do loop repeats a tactic :token:`nat_or_var` times:
 
@@ -497,7 +498,6 @@ Repeat loop
 ~~~~~~~~~~~
 
 .. tacn:: repeat @ltac_expr3
-   :name: repeat
 
    The repeat loop repeats a tactic until it fails.
 
@@ -515,7 +515,6 @@ Catching errors: try
 We can catch the tactic errors with:
 
 .. tacn:: try @ltac_expr3
-   :name: try
 
    :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic
    value ``v`` is applied to each focused goal independently. If the application of
@@ -531,7 +530,6 @@ Detecting progress
 We can check if a tactic made progress with:
 
 .. tacn:: progress @ltac_expr3
-   :name: progress
 
    :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v``
    is applied to each focused subgoal independently. If the application of ``v``
@@ -641,7 +639,6 @@ First tactic to succeed
 In some cases backtracking may be too expensive.
 
 .. tacn:: first [ {*| @ltac_expr } ]
-   :name: first
 
    For each focused goal, independently apply the first :token:`ltac_expr` that succeeds.
    The :n:`@ltac_expr`\s must evaluate to tactic values.
@@ -701,7 +698,6 @@ Selects and applies the first tactic that solves each goal (i.e. leaves no subgo
 in a series of alternative tactics:
 
 .. tacn:: solve [ {*| @ltac_expr__i } ]
-   :name: solve
 
    For each current subgoal: evaluates and applies each :n:`@ltac_expr` in order
    until one is found that solves the subgoal.
@@ -743,7 +739,6 @@ Conditional branching: tryif
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: tryif @ltac_expr__test then @ltac_expr__then else @ltac_expr2__else
-   :name: tryif
 
    For each focused goal, independently: Evaluate and apply :n:`@ltac_expr__test`.
    If :n:`@ltac_expr__test` succeeds at least once, evaluate and apply :n:`@ltac_expr__then`
@@ -772,7 +767,6 @@ Another way of restricting backtracking is to restrict a tactic to a
 single success:
 
 .. tacn:: once @ltac_expr3
-   :name: once
 
    :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied but only its first success is used. If ``v`` fails,
@@ -788,7 +782,6 @@ Coq provides an experimental way to check that a tactic has *exactly
 one* success:
 
 .. tacn:: exactly_once @ltac_expr3
-   :name: exactly_once
 
    :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied if it has at most one success. If ``v`` fails,
@@ -816,7 +809,6 @@ Checking for failure: assert_fails
 Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*:
 
 .. tacn:: assert_fails @ltac_expr3
-   :name: assert_fails
 
    If :n:`@ltac_expr3` fails, the proof state is unchanged and no message is printed.
    If :n:`@ltac_expr3` unexpectedly has at least one success, the tactic performs
@@ -863,7 +855,6 @@ Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at le
 success:
 
 .. tacn:: assert_succeeds @ltac_expr3
-   :name: assert_succeeds
 
    If :n:`@ltac_expr3` has at least one success, the proof state is unchanged and
    no message is printed.  If :n:`@ltac_expr3` fails, the tactic performs
@@ -877,7 +868,6 @@ Print/identity tactic: idtac
 
 
 .. tacn:: idtac {* {| @ident | @string | @natural } }
-   :name: idtac
 
    Leaves the proof unchanged and prints the given tokens. :token:`String<string>`\s
    and :token:`natural`\s are printed
@@ -974,7 +964,6 @@ We can force a tactic to stop if it has not finished after a certain
 amount of time:
 
 .. tacn:: timeout @nat_or_var @ltac_expr3
-   :name: timeout
 
    :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
    ``v`` is applied normally, except that it is interrupted after :n:`@nat_or_var` seconds
@@ -998,7 +987,6 @@ Timing a tactic
 A tactic execution can be timed:
 
 .. tacn:: time {? @string } @ltac_expr3
-   :name: time
 
    evaluates :n:`@ltac_expr3` and displays the running time of the tactic expression, whether it
    fails or succeeds. In case of several successes, the time for each successive
@@ -1015,7 +1003,6 @@ Tactic expressions that produce terms can be timed with the experimental
 tactic
 
 .. tacn:: time_constr @ltac_expr
-   :name: time_constr
 
    which evaluates :n:`@ltac_expr ()` and displays the time the tactic expression
    evaluated, assuming successful evaluation. Time is in seconds and is
@@ -1026,12 +1013,10 @@ tactic
    implemented using the following internal tactics:
 
 .. tacn:: restart_timer {? @string }
-   :name: restart_timer
 
    Reset a timer
 
 .. tacn:: finish_timing {? ( @string ) } {? @string }
-   :name: finish_timing
 
    Display an optionally named timer. The parenthesized string argument
    is also optional, and determines the label associated with the timer
@@ -1362,7 +1347,7 @@ Pattern matching on goals and hypotheses: match goal
 
    :tacn:`lazymatch goal`, :tacn:`match goal` and :tacn:`multimatch goal` are :token:`l1_tactic`\s.
 
-   Use this form to match hypotheses and/or goals in the proof context.  These patterns have zero or
+   Use this form to match hypotheses and/or goals in the local context.  These patterns have zero or
    more subpatterns to match hypotheses followed by a subpattern to match the conclusion.  Except for the
    differences noted below, this works the same as the corresponding :n:`@match_key @ltac_expr` construct
    (see :tacn:`match`).  Each current goal is processed independently.
@@ -1533,7 +1518,7 @@ expression returns an identifier:
    .. todo you can't have a :tacn: with the same name as a :gdef: for now,
       eg `fresh` can't be both
 
-   Returns a fresh identifier name (i.e. one that is not already used in the context
+   Returns a fresh identifier name (i.e. one that is not already used in the local context
    and not previously returned by :tacn:`fresh` in the current :token:`ltac_expr`).
    The fresh identifier is formed by concatenating the final :token:`ident` of each :token:`qualid`
    (dropping any qualified components) and each specified :token:`string`.
@@ -1541,11 +1526,11 @@ expression returns an identifier:
    If no arguments are given, the name is a fresh derivative of the name ``H``.
 
    .. note:: We recommend generating the fresh identifier immediately before
-      adding it in the proof context.  Using :tacn:`fresh` in a local function
+      adding it to the local context.  Using :tacn:`fresh` in a local function
       may not work as you expect:
 
-      Successive :tacn:`fresh`\es give distinct names even if the names haven't
-      yet been added to the proof context:
+      Successive calls to :tacn:`fresh` give distinct names even if the names haven't
+      yet been added to the local context:
 
       .. coqtop:: reset none
 
@@ -1635,7 +1620,6 @@ Testing boolean expressions: guard
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: guard @int_or_var @comparison @int_or_var
-   :name: guard
 
    .. insertprodn int_or_var comparison
 
@@ -1734,7 +1718,6 @@ Defining |Ltac| symbols
 .. index:: ::=
 
 .. cmd:: Ltac @tacdef_body {* with @tacdef_body }
-   :name: Ltac
 
    .. insertprodn tacdef_body tacdef_body
 
@@ -2248,7 +2231,6 @@ Tracing execution
    not printed.
 
    .. opt:: Info Level @natural
-      :name: Info Level
 
       This option is an alternative to the :cmd:`Info` command.
 
@@ -2269,17 +2251,17 @@ The debugger stops, prompting for a command which can be one of the
 following:
 
 +-----------------+-----------------------------------------------+
-| simple newline: | go to the next step                           |
+| newline         | go to the next step                           |
 +-----------------+-----------------------------------------------+
-| h:              | get help                                      |
+| h               | get help                                      |
 +-----------------+-----------------------------------------------+
-| x:              | exit current evaluation                       |
+| r n             | advance n steps further                       |
 +-----------------+-----------------------------------------------+
-| s:              | continue current evaluation without stopping  |
+| r string        | advance up to the next call to “idtac string” |
 +-----------------+-----------------------------------------------+
-| r n:            | advance n steps further                       |
+| s               | continue current evaluation without stopping  |
 +-----------------+-----------------------------------------------+
-| r string:       | advance up to the next call to “idtac string” |
+| x               | exit current evaluation                       |
 +-----------------+-----------------------------------------------+
 
 .. exn:: Debug mode not available in the IDE
@@ -2366,25 +2348,21 @@ performance issue.
    Unset Ltac Profiling.
 
 .. tacn:: start ltac profiling
-   :name: start ltac profiling
 
    This tactic behaves like :tacn:`idtac` but enables the profiler.
 
 .. tacn:: stop ltac profiling
-   :name: stop ltac profiling
 
    Similarly to :tacn:`start ltac profiling`, this tactic behaves like
    :tacn:`idtac`. Together, they allow you to exclude parts of a proof script
    from profiling.
 
 .. tacn:: reset ltac profile
-   :name: reset ltac profile
 
    Equivalent to the :cmd:`Reset Ltac Profile` command, which allows
    resetting the profile from tactic scripts for benchmarking purposes.
 
 .. tacn:: show ltac profile {? {| cutoff @integer | @string } }
-   :name: show ltac profile
 
    Equivalent to the :cmd:`Show Ltac Profile` command,
    which allows displaying the profile from tactic scripts for
@@ -2410,11 +2388,10 @@ Run-time optimization tactic
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. tacn:: optimize_heap
-   :name: optimize_heap
 
    This tactic behaves like :tacn:`idtac`, except that running it compacts the
-   heap in the OCaml run-time system. It is analogous to the Vernacular
-   command :cmd:`Optimize Heap`.
+   heap in the OCaml run-time system. It is analogous to the
+   :cmd:`Optimize Heap` command.
 
 .. tacn:: infoH @ltac_expr3
 
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 375129c02d..3646a32a79 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -173,7 +173,6 @@ Type declarations
 One can define new types with the following commands.
 
 .. cmd:: Ltac2 Type {? rec } @tac2typ_def {* with @tac2typ_def }
-   :name: Ltac2 Type
 
    .. insertprodn tac2typ_def tac2rec_field
 
@@ -301,7 +300,6 @@ Ltac2 Definitions
 ~~~~~~~~~~~~~~~~~
 
 .. cmd:: Ltac2 {? mutable } {? rec } @tac2def_body {* with @tac2def_body }
-   :name: Ltac2
 
    .. insertprodn tac2def_body tac2def_body
 
@@ -322,7 +320,6 @@ Ltac2 Definitions
    If ``mutable`` is set, the definition can be redefined at a later stage (see below).
 
 .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr
-   :name: Ltac2 Set
 
    This command redefines a previous ``mutable`` definition.
    Mutable definitions act like dynamic binding, i.e. at runtime, the last defined
@@ -598,7 +595,7 @@ modes, the *strict* and the *non-strict* mode.
   hypotheses. If this doesn't hold, internalization will fail. To work around
   this error, one has to specifically use the ``&`` notation.
 - In non-strict mode, any simple identifier appearing in a term quotation which
-  is not bound in the global context is turned into a dynamic reference to a
+  is not bound in the global environment is turned into a dynamic reference to a
   hypothesis. That is to say, internalization will succeed, but the evaluation
   of the term at runtime will fail if there is no such variable in the dynamic
   context.
@@ -982,7 +979,7 @@ Match over goals
       gmatch_hyp_pattern ::= @name : @ltac2_match_pattern
 
    Matches over goals, similar to Ltac1 :tacn:`match goal`.
-   Use this form to match hypotheses and/or goals in the proof context.  These patterns have zero or
+   Use this form to match hypotheses and/or goals in the local context.  These patterns have zero or
    more subpatterns to match hypotheses followed by a subpattern to match the conclusion.  Except for the
    differences noted below, this works the same as the corresponding :n:`@ltac2_match_key @ltac2_expr` construct
    (see :tacn:`match!`).  Each current goal is processed independently.
@@ -1164,7 +1161,6 @@ Notations
 ---------
 
 .. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr
-   :name: Ltac2 Notation
 
    .. todo seems like name maybe should use lident rather than ident, considering:
 
@@ -1487,7 +1483,7 @@ Other nonterminals that have syntactic classes are listed here.
 
       * - :n:`conversion`
         - :token:`ltac2_conversion`
-        - :token:`conversion`
+        -
 
       * - :n:`rewriting`
         - :token:`ltac2_oriented_rewriter`
@@ -1679,7 +1675,6 @@ Evaluation
 Ltac2 features a toplevel loop that can be used to evaluate expressions.
 
 .. cmd:: Ltac2 Eval @ltac2_expr
-   :name: Ltac2 Eval
 
    This command evaluates the term in the current proof if there is one, or in the
    global environment otherwise, and displays the resulting value to the user
@@ -1877,9 +1872,9 @@ In Ltac expressions
 
 .. exn:: Unbound {| value | constructor } X
 
-   * if `X` is meant to be a term from the current stactic environment, replace
+   * if `X` is meant to be a term from the current static environment, replace
      the problematic use by `'X`.
-   * if `X` is meant to be a hypothesis from the goal context, replace the
+   * if `X` is meant to be a hypothesis from the local context, replace the
      problematic use by `&X`.
 
 In quotations
@@ -1889,7 +1884,7 @@ In quotations
 
    * if `X` is meant to be a tactic expression bound by a Ltac2 let or function,
      replace the problematic use by `$X`.
-   * if `X` is meant to be a hypothesis from the goal context, replace the
+   * if `X` is meant to be a hypothesis from the local context, replace the
      problematic use by `&X`.
 
 Exception catching
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 07c2d268c6..bab9d35099 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -116,8 +116,8 @@ compatible with the rest of Coq, up to a few discrepancies:
 
 
 + New keywords (``is``) might clash with variable, constant, tactic or
-  tactical names, or with quasi-keywords in tactic or vernacular
-  notations.
+  tactical names, or with quasi-keywords in tactic or
+  notation commands.
 + New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`,
   :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`)
   might clash with user tactic names.
@@ -799,8 +799,9 @@ An *occurrence switch* can be:
         set x := {+1 3}(f 2).
 
   Notice that some occurrences of a given term may be
-  hidden to the user, for example because of a notation. The vernacular
-  ``Set Printing All`` command displays all these hidden occurrences and
+  hidden to the user, for example because of a notation. Setting the
+  :flag:`Printing All` flag causes these hidden occurrences to
+  be shown when the term is displayed.  This setting
   should be used to find the correct coding of the occurrences to be
   selected [#1]_.
 
@@ -1023,7 +1024,7 @@ conversely in between deductive steps.
 
 In |SSR| these moves are performed by two *tacticals* ``=>`` and
 ``:``, so that the bookkeeping required by a deductive step can be
-directly associated to that step, and that tactics in an |SSR|
+directly associated with that step, and that tactics in an |SSR|
 script correspond to actual logical steps in the proof rather than
 merely shuffle facts. Still, some isolated bookkeeping is unavoidable,
 such as naming variables and assumptions at the beginning of a
@@ -1189,7 +1190,7 @@ The move tactic.
 ````````````````
 
 .. tacn:: move
-   :name: move
+   :name: move (ssreflect)
 
    This tactic, in its defective form, behaves like the :tacn:`hnf` tactic.
 
@@ -5502,7 +5503,7 @@ equivalences are indeed taken into account, otherwise only single
      string that contains symbols or is followed by a scope key, is
      interpreted as the constant whose notation involves that string (e.g.,
      :g:`+` for :g:`addn`), if this is unambiguous; otherwise the diagnostic
-     includes the output of the :cmd:`Locate` vernacular command.
+     includes the output of the :cmd:`Locate` command.
    + whose statement, including assumptions and types, contains a subterm
      matching the next patterns. If a pattern is prefixed by ``-``, the test is
      reversed;
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index d8c4fb61c2..a750ce2892 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3,35 +3,46 @@
 Tactics
 ========
 
-A deduction rule is a link between some (unique) formula, that we call
-the *conclusion* and (several) formulas that we call the *premises*. A
-deduction rule can be read in two ways. The first one says: “if I know
-this and this then I can deduce this”. For instance, if I have a proof
-of A and a proof of B then I have a proof of A ∧ B. This is forward
-reasoning from premises to conclusion. The other way says: “to prove
-this I have to prove this and this”. For instance, to prove A ∧ B, I
-have to prove A and I have to prove B. This is backward reasoning from
-conclusion to premises. We say that the conclusion is the *goal* to
-prove and premises are the *subgoals*. The tactics implement *backward
-reasoning*. When applied to a goal, a tactic replaces this goal with
-the subgoals it generates. We say that a tactic reduces a goal to its
-subgoal(s).
-
-Each (sub)goal is denoted with a number. The current goal is numbered
-1. By default, a tactic is applied to the current goal, but one can
-address a particular goal in the list by writing n:tactic which means
-“apply tactic tactic to goal number n”. We can show the list of
-subgoals by typing Show (see Section :ref:`requestinginformation`).
-
-Since not every rule applies to a given statement, not every tactic can
-be used to reduce a given goal. In other words, before applying a tactic
-to a given goal, the system checks that some *preconditions* are
-satisfied. If it is not the case, the tactic raises an error message.
-
-Tactics are built from atomic tactics and tactic expressions (which
-extends the folklore notion of tactical) to combine those atomic
-tactics. This chapter is devoted to atomic tactics. The tactic
-language will be described in Chapter :ref:`ltac`.
+Tactics specify how to transform the :term:`proof state` of an
+incomplete proof to eventually generate a complete proof.
+
+Proofs can be developed in two basic ways: In :gdef:`forward reasoning`,
+the proof begins by proving simple statements that are then combined to prove the
+theorem statement as the last step of the proof. With forward reasoning,
+for example,
+the proof of `A /\\ B` would begin with proofs of `A` and `B`, which are
+then used to prove `A /\\ B`.  Forward reasoning is probably the most common
+approach in human-generated proofs.
+
+In :gdef:`backward reasoning`, the proof begins with the theorem statement
+as the goal, which is then gradually transformed until every subgoal generated
+along the way has been proven.  In this case, the proof of `A /\\ B` begins
+with that formula as the goal.  This can be transformed into two subgoals,
+`A` and `B`, followed by the proofs of `A` and `B`.  Coq and its tactics
+use backward reasoning.
+
+A tactic may fully prove a goal, in which case the goal is removed
+from the proof state.
+More commonly, a tactic replaces a goal with one or more :term:`subgoals <subgoal>`.
+(We say that a tactic reduces a goal to its subgoals.)
+
+Most tactics require specific elements or preconditions to reduce a goal;
+they display error messages if they can't be applied to the goal.
+A few tactics, such as :tacn:`auto`, don't fail even if the proof state
+is unchanged.
+
+Goals are identified by number. The current goal is number
+1. Tactics are applied to the current goal by default.  (The
+default can be changed with the :opt:`Default Goal Selector`
+option.)  They can
+be applied to another goal or to multiple goals with a
+:ref:`goal selector <goal-selectors>` such as :n:`2: @tactic`.
+
+This chapter describes many of the most common built-in tactics.
+Built-in tactics can be combined to form tactic expressions, which are
+described in the :ref:`Ltac` chapter.  Since tactic expressions can
+be used anywhere that a built-in tactic can be used, "tactic" may
+refer to both built-in tactics and tactic expressions.
 
 Common elements of tactics
 --------------------------
@@ -529,8 +540,21 @@ one or more of its hypotheses.
    which is equivalent to `in * |- *`.  Use `* |-` to select all occurrences
    in all hypotheses.
 
-Tactics that use occurrence clauses include :tacn:`set`,
-:tacn:`remember`, :tacn:`induction` and :tacn:`destruct`.
+   Tactics that select a specific hypothesis H to apply to other hypotheses,
+   such as :tacn:`rewrite` `H in * |-`, won't apply H to itself.
+
+   If multiple
+   occurrences are given, such as in :tacn:`rewrite` `H at 1 2 3`, the tactic
+   must match at least one occurrence in order to succeed.  The tactic will fail
+   if no occurrences match.  Occurrence numbers that are out of range (e.g.
+   `at 1 3` when there are only 2 occurrences in the hypothesis or conclusion)
+   are ignored.
+
+   .. todo: remove last sentence above and add "Invalid occurrence number @natural" exn for 8.14
+      per #13568.
+
+   Tactics that use occurrence clauses include :tacn:`set`,
+   :tacn:`remember`, :tacn:`induction` and :tacn:`destruct`.
 
 
 .. seealso::
@@ -1979,7 +2003,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    This is a more basic induction tactic. Again, the type of the argument
    :n:`@term` must be an inductive type. Then, according to the type of the
    goal, the tactic ``elim`` chooses the appropriate destructor and applies it
-   as the tactic :tacn:`apply` would do. For instance, if the proof context
+   as the tactic :tacn:`apply` would do. For instance, if the local context
    contains :g:`n:nat` and the current goal is :g:`T` of type :g:`Prop`, then
    :n:`elim n` is equivalent to :n:`apply nat_ind with (n:=n)`. The tactic
    ``elim`` does not modify the context of the goal, neither introduces the
@@ -2651,7 +2675,7 @@ and an explanation of the underlying technique.
    Like in a fix expression, the induction hypotheses have to be used on
    structurally smaller arguments. The verification that inductive proof
    arguments are correct is done only at the time of registering the
-   lemma in the environment. To know if the use of induction hypotheses
+   lemma in the global environment. To know if the use of induction hypotheses
    is correct at some time of the interactive development of a proof, use
    the command ``Guarded`` (see Section :ref:`requestinginformation`).
 
@@ -2671,7 +2695,7 @@ and an explanation of the underlying technique.
    name given to the coinduction hypothesis. Like in a cofix expression,
    the use of induction hypotheses have to guarded by a constructor. The
    verification that the use of co-inductive hypotheses is correct is
-   done only at the time of registering the lemma in the environment. To
+   done only at the time of registering the lemma in the global environment. To
    know if the use of coinduction hypotheses is correct at some time of
    the interactive development of a proof, use the command ``Guarded``
    (see Section :ref:`requestinginformation`).
@@ -2752,14 +2776,11 @@ succeeds, and results in an error otherwise.
    :name: is_var
 
    This tactic checks whether its argument is a variable or hypothesis in
-   the current goal context or in the opened sections.
+   the current local context.
 
 .. exn:: Not a variable or hypothesis.
    :undocumented:
 
-
-.. _equality:
-
 Equality
 --------
 
@@ -2954,59 +2975,7 @@ references to automatically generated names.
 Performance-oriented tactic variants
 ------------------------------------
 
-.. tacn:: change_no_check @term
-   :name: change_no_check
-
-   For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization,
-   it skips checking that :n:`@term` is convertible to the goal.
-
-   Recall that the Coq kernel typechecks proofs again when they are concluded to
-   ensure safety. Hence, using :tacn:`change` checks convertibility twice
-   overall, while :tacn:`change_no_check` can produce ill-typed terms,
-   but checks convertibility only once.
-   Hence, :tacn:`change_no_check` can be useful to speed up certain proof
-   scripts, especially if one knows by construction that the argument is
-   indeed convertible to the goal.
-
-   In the following example, :tacn:`change_no_check` replaces :g:`False` by
-   :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency.
-
-   .. example::
-
-      .. coqtop:: all abort
-
-         Goal False.
-           change_no_check True.
-           exact I.
-         Fail Qed.
-
-   :tacn:`change_no_check` supports all of :tacn:`change`'s variants.
-
-   .. tacv:: change_no_check @term with @term’
-      :undocumented:
-
-   .. tacv:: change_no_check @term at {+ @natural} with @term’
-      :undocumented:
-
-   .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident
-
-      .. example::
-
-         .. coqtop:: all abort
-
-            Goal True -> False.
-              intro H.
-              change_no_check False in H.
-              exact H.
-            Fail Qed.
-
-   .. tacv:: convert_concl_no_check @term
-      :name: convert_concl_no_check
-
-      .. deprecated:: 8.11
-
-      Deprecated old name for :tacn:`change_no_check`. Does not support any of its
-      variants.
+.. todo: move the following adjacent to the `exact` tactic in the rewriting chapter?
 
 .. tacn:: exact_no_check @term
    :name: exact_no_check
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e866e4c624..8e2f577f6b 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1,7 +1,7 @@
 .. _vernacularcommands:
 
-Vernacular commands
-=============================
+Commands
+========
 
 .. _displaying:
 
@@ -60,7 +60,7 @@ Query commands
 --------------
 
 Unlike other commands, :production:`query_command`\s may be prefixed with
-a goal selector (:n:`@natural:`) to specify which goal context it applies to.
+a goal selector (:n:`@natural:`) to specify which goals it applies to.
 If no selector is provided,
 the command applies to the current goal.  If no proof is open, then the command only applies
 to accessible objects.  (see Section :ref:`invocation-of-tactics`).
@@ -382,7 +382,6 @@ to accessible objects.  (see Section :ref:`invocation-of-tactics`).
          SearchRewrite (_ + _ + _).
 
 .. table:: Search Blacklist @string
-   :name: Search Blacklist
 
    Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,
    :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries.  A lemma whose
@@ -668,8 +667,8 @@ Loadpath
 ------------
 
 Loadpaths are preferably managed using Coq command line options (see
-Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them
-for practical purposes. Such commands are only meant to be issued in
+Section :ref:`libraries-and-filesystem`), but there are also commands
+to manage them within Coq. These commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
 
 
@@ -740,7 +739,7 @@ Backtracking
 ------------
 
 The backtracking commands described in this section can only be used
-interactively, they cannot be part of a vernacular file loaded via
+interactively, they cannot be part of a Coq file loaded via
 ``Load`` or compiled by ``coqc``.
 
 
@@ -844,7 +843,6 @@ Quitting and debugging
    displayed.
 
    .. opt:: Default Timeout @natural
-      :name: Default Timeout
 
       If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@natural`,
       except for :cmd:`Timeout` commands themselves.  If unset,
@@ -883,7 +881,6 @@ Controlling display
    This flag controls the normal displaying.
 
 .. opt:: Warnings "{+, {? {| - | + } } @ident }"
-   :name: Warnings
 
    This option configures the display of warnings. It is experimental, and
    expects, between quotes, a comma-separated list of warning names or
@@ -894,14 +891,12 @@ Controlling display
    right have higher priority, meaning that `A,-A` is equivalent to `-A`.
 
 .. opt:: Printing Width @natural
-   :name: Printing Width
 
    This command sets which left-aligned part of the width of the screen is used
    for display. At the time of writing this documentation, the default value
    is 78.
 
 .. opt:: Printing Depth @natural
-   :name: Printing Depth
 
    This option controls the nesting depth of the formatter used for pretty-
    printing. Beyond this depth, display of subterms is replaced by dots. At the