Merge content from two origins into the same file.

2 files changed, 935 insertions, 927 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
deleted file mode 100644
index f4aef8f879..0000000000
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ /dev/null
@@ -1,927 +0,0 @@
-.. _proofhandling:
-
--------------------
- Proof handling
--------------------
-
-In |Coq|’s proof editing mode all top-level commands documented in
-Chapter :ref:`vernacularcommands` remain available and the user has access to specialized
-commands dealing with proof development pragmas documented in this
-section. They can also use some other specialized commands called
-*tactics*. They are the very tools allowing the user to deal with
-logical reasoning. They are documented in Chapter :ref:`tactics`.
-
-|Coq| user interfaces usually have a way of marking whether the user has
-switched to proof editing mode. For instance, in coqtop the prompt ``Coq <``   is changed into
-:n:`@ident <`   where :token:`ident` is the declared name of the theorem currently edited.
-
-At each stage of a proof development, one has a list of goals to
-prove. Initially, the list consists only in the theorem itself. After
-having applied some tactics, the list of goals contains the subgoals
-generated by the tactics.
-
-To each subgoal is associated a number of hypotheses called the *local context*
-of the goal. Initially, the local context contains the local variables and
-hypotheses of the current section (see Section :ref:`gallina-assumptions`) and
-the local variables and hypotheses of the theorem statement. It is enriched by
-the use of certain tactics (see e.g. :tacn:`intro`).
-
-When a proof is completed, the message ``Proof completed`` is displayed.
-One can then register this proof as a defined constant in the
-environment. Because there exists a correspondence between proofs and
-terms of λ-calculus, known as the *Curry-Howard isomorphism*
-:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those
-terms are called *proof terms*.
-
-
-.. exn:: No focused proof.
-
-   |Coq| raises this error message when one attempts to use a proof editing command
-   out of the proof editing mode.
-
-.. _proof-editing-mode:
-
-Entering and leaving proof editing mode
----------------------------------------
-
-The proof editing mode is entered by asserting a statement, which typically is
-the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
-list of assertion commands is given in :ref:`Assertions`. The command
-:cmd:`Goal` can also be used.
-
-.. cmd:: Goal @type
-
-   This is intended for quick assertion of statements, without knowing in
-   advance which name to give to the assertion, typically for quick
-   testing of the provability of a statement. If the proof of the
-   statement is eventually completed and validated, the statement is then
-   bound to the name ``Unnamed_thm`` (or a variant of this name not already
-   used for another statement).
-
-.. cmd:: Qed
-
-   This command is available in interactive editing proof mode when the
-   proof is completed. Then :cmd:`Qed` extracts a proof term from the proof
-   script, switches back to |Coq| top-level and attaches the extracted
-   proof term to the declared name of the original goal. The name is
-   added to the environment as an opaque constant.
-
-   .. exn:: Attempt to save an incomplete proof.
-      :undocumented:
-
-   .. note::
-
-      Sometimes an error occurs when building the proof term, because
-      tactics do not enforce completely the term construction
-      constraints.
-
-      The user should also be aware of the fact that since the
-      proof term is completely rechecked at this point, one may have to wait
-      a while when the proof is large. In some exceptional cases one may
-      even incur a memory overflow.
-
-.. cmd:: Save @ident
-   :name: Save
-
-   Saves a completed proof with the name :token:`ident`, which
-   overrides any name provided by the :cmd:`Theorem` command or
-   its variants.
-
-.. cmd:: Defined {? @ident }
-
-   Similar to :cmd:`Qed` and :cmd:`Save`, except the proof is made *transparent*, which means
-   that its content can be explicitly used for type checking and that it can be
-   unfolded in conversion tactics (see :ref:`performingcomputations`,
-   :cmd:`Opaque`, :cmd:`Transparent`).  If :token:`ident` is specified,
-   the proof is defined with the given name, which overrides any name
-   provided by the :cmd:`Theorem` command or its variants.
-
-.. cmd:: Admitted
-
-   This command is available in interactive editing mode to give up
-   the current proof and declare the initial goal as an axiom.
-
-.. cmd:: Abort {? {| All | @ident } }
-
-   Cancels the current proof development, switching back to
-   the previous proof development, or to the |Coq| toplevel if no other
-   proof was being edited.
-
-   :n:`@ident`
-     Aborts editing the proof named :n:`@ident` for use when you have
-     nested proofs.  See also :flag:`Nested Proofs Allowed`.
-
-   :n:`All`
-     Aborts all current proofs.
-
-   .. exn:: No focused proof (No proof-editing in progress).
-      :undocumented:
-
-.. cmd:: Proof @term
-   :name: Proof `term`
-
-   This command applies in proof editing mode. It is equivalent to
-   :n:`exact @term. Qed.`
-   That is, you have to give the full proof in one gulp, as a
-   proof term (see Section :ref:`applyingtheorems`).
-
-   .. warning::
-
-      Use of this command is discouraged.  In particular, it
-      doesn't work in Proof General because it must
-      immediately follow the command that opened proof mode, but
-      Proof General inserts :cmd:`Unset` :flag:`Silent` before it (see
-      `Proof General issue #498
-      <https://github.com/ProofGeneral/PG/issues/498>`_).
-
-.. cmd:: Proof
-
-   Is a no-op which is useful to delimit the sequence of tactic commands
-   which start a proof, after a :cmd:`Theorem` command. It is a good practice to
-   use :cmd:`Proof` as an opening parenthesis, closed in the script with a
-   closing :cmd:`Qed`.
-
-   .. seealso:: :cmd:`Proof with`
-
-.. cmd:: Proof using @section_var_expr {? with @ltac_expr }
-
-   .. insertprodn section_var_expr starred_ident_ref
-
-   .. prodn::
-      section_var_expr ::= {* @starred_ident_ref }
-      | {? - } @section_var_expr50
-      section_var_expr50 ::= @section_var_expr0 - @section_var_expr0
-      | @section_var_expr0 + @section_var_expr0
-      | @section_var_expr0
-      section_var_expr0 ::= @starred_ident_ref
-      | ( @section_var_expr ) {? * }
-      starred_ident_ref ::= @ident {? * }
-      | Type {? * }
-      | All
-
-   Opens proof editing mode, declaring the set of
-   section variables (see :ref:`gallina-assumptions`) used by the proof.
-   At :cmd:`Qed` time, the
-   system verifies that the set of section variables used in
-   the proof is a subset of the declared one.
-
-   The set of declared variables is closed under type dependency. For
-   example, if ``T`` is a variable and ``a`` is a variable of type
-   ``T``, then the commands ``Proof using a`` and ``Proof using T a``
-   are equivalent.
-
-   The set of declared variables always includes the variables used by
-   the statement. In other words ``Proof using e`` is equivalent to
-   ``Proof using Type + e`` for any declaration expression ``e``.
-
-   :n:`- @section_var_expr50`
-     Use all section variables except those specified by :n:`@section_var_expr50`
-
-   :n:`@section_var_expr0 + @section_var_expr0`
-     Use section variables from the union of both collections.
-     See :ref:`nameaset` to see how to form a named collection.
-
-   :n:`@section_var_expr0 - @section_var_expr0`
-     Use section variables which are in the first collection but not in the
-     second one.
-
-   :n:`{? * }`
-     Use the transitive closure of the specified collection.
-
-   :n:`Type`
-     Use only section variables occurring in the statement.  Specifying :n:`*`
-     uses the forward transitive closure of all the section variables occurring
-     in the statement. For example, if the variable ``H`` has type ``p < 5`` then
-     ``H`` is in ``p*`` since ``p`` occurs in the type of ``H``.
-
-   :n:`All`
-     Use all section variables.
-
-   .. seealso:: :ref:`tactics-implicit-automation`
-
-.. attr:: using
-
-   This attribute can be applied to the :cmd:`Definition`, :cmd:`Example`,
-   :cmd:`Fixpoint` and :cmd:`CoFixpoint` commands as well as to :cmd:`Lemma` and
-   its variants.  It takes
-   a :n:`@section_var_expr`, in quotes, as its value. This is equivalent to
-   specifying the same :n:`@section_var_expr` in
-   :cmd:`Proof using`.
-
-   .. example::
-
-      .. coqtop:: all
-
-         Section Test.
-         Variable n : nat.
-         Hypothesis Hn : n <> 0.
-
-         #[using="Hn"]
-         Lemma example : 0 < n.
-
-      .. coqtop:: in
-
-         Abort.
-         End Test.
-
-
-Proof using options
-```````````````````
-
-The following options modify the behavior of ``Proof using``.
-
-
-.. opt:: Default Proof Using "@section_var_expr"
-   :name: Default Proof Using
-
-   Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default
-   Proof Using "a b"`` will complete all ``Proof`` commands not followed by a
-   ``using`` part with ``using a b``.
-
-
-.. flag:: Suggest Proof Using
-
-   When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not
-   provide one.
-
-..  _`nameaset`:
-
-Name a set of section hypotheses for ``Proof using``
-````````````````````````````````````````````````````
-
-.. cmd:: Collection @ident := @section_var_expr
-
-   This can be used to name a set of section
-   hypotheses, with the purpose of making ``Proof using`` annotations more
-   compact.
-
-   .. example::
-
-      Define the collection named ``Some`` containing ``x``, ``y`` and ``z``::
-
-         Collection Some := x y z.
-
-      Define the collection named ``Fewer`` containing only ``x`` and ``y``::
-
-         Collection Fewer := Some - z
-
-      Define the collection named ``Many`` containing the set union or set
-      difference of ``Fewer`` and ``Some``::
-
-         Collection Many := Fewer + Some
-         Collection Many := Fewer - Some
-
-      Define the collection named ``Many`` containing the set difference of
-      ``Fewer`` and the unnamed collection ``x y``::
-
-         Collection Many := Fewer - (x y)
-
-
-
-.. cmd:: Existential @natural {? : @type } := @term
-
-   This command instantiates an existential variable. :token:`natural` is an index in
-   the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`.
-
-   This command is intended to be used to instantiate existential
-   variables when the proof is completed but some uninstantiated
-   existential variables remain. To instantiate existential variables
-   during proof edition, you should use the tactic :tacn:`instantiate`.
-
-.. cmd:: Grab Existential Variables
-
-   This command can be run when a proof has no more goal to be solved but
-   has remaining uninstantiated existential variables. It takes every
-   uninstantiated existential variable and turns it into a goal.
-
-Proof modes
-```````````
-
-When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`,
-|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes
-shipped in the standard |Coq| installation, and furthermore some plugins define
-their own proof modes. The default proof mode used when opening a proof can
-be changed using the following option.
-
-.. opt:: Default Proof Mode @string
-
-   Select the proof mode to use when starting a proof. Depending on the proof
-   mode, various syntactic constructs are allowed when writing an interactive
-   proof. All proof modes support vernacular commands; the proof mode determines
-   which tactic language and set of tactic definitions are available.  The
-   possible option values are:
-
-   `"Classic"`
-     Activates the |Ltac| language and the tactics with the syntax documented
-     in this manual.
-     Some tactics are not available until the associated plugin is loaded,
-     such as `SSR` or `micromega`.
-     This proof mode is set when the :term:`prelude` is loaded.
-
-   `"Noedit"`
-     No tactic
-     language is activated at all. This is the default when the :term:`prelude`
-     is not loaded, e.g. through the `-noinit` option for `coqc`.
-
-   `"Ltac2"`
-     Activates the Ltac2 language and the Ltac2-specific variants of the documented
-     tactics.
-     This value is only available after :cmd:`Requiring <Require>` Ltac2.
-     :cmd:`Importing <Import>` Ltac2 sets this mode.
-
-   Some external plugins also define their own proof mode, which can be
-   activated with this command.
-
-Navigation in the proof tree
---------------------------------
-
-.. cmd:: Undo {? {? To } @natural }
-
-   Cancels the effect of the last :token:`natural` commands or tactics.
-   The :n:`To @natural` form goes back to the specified state number.
-   If :token:`natural` is not specified, the command goes back one command or tactic.
-
-.. cmd:: Restart
-
-   Restores the proof editing process to the original goal.
-
-   .. exn:: No focused proof to restart.
-      :undocumented:
-
-.. cmd:: Focus {? @natural }
-
-   Focuses the attention on the first subgoal to prove or, if :token:`natural` is
-   specified, the :token:`natural`\-th.  The
-   printing of the other subgoals is suspended until the focused subgoal
-   is solved or unfocused.
-
-   .. deprecated:: 8.8
-
-      Prefer the use of bullets or focusing brackets with a goal selector (see below).
-
-.. cmd:: Unfocus
-
-   This command restores to focus the goal that were suspended by the
-   last :cmd:`Focus` command.
-
-   .. deprecated:: 8.8
-
-.. cmd:: Unfocused
-
-   Succeeds if the proof is fully unfocused, fails if there are some
-   goals out of focus.
-
-.. _curly-braces:
-
-.. index:: {
-           }
-
-.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket,
-   hence the verbose names
-
-.. tacn:: {? {| @natural | [ @ident ] } : } %{
-         %}
-
-   .. todo
-      See https://github.com/coq/coq/issues/12004 and
-      https://github.com/coq/coq/issues/12825.
-
-   ``{`` (without a terminating period) focuses on the first
-   goal.  The subproof can only be
-   unfocused when it has been fully solved (*i.e.*, when there is no
-   focused goal left). Unfocusing is then handled by ``}`` (again, without a
-   terminating period). See also an example in the next section.
-
-   Note that when a focused goal is proved a message is displayed
-   together with a suggestion about the right bullet or ``}`` to unfocus it
-   or focus the next one.
-
-   :n:`@natural:`
-     Focuses on the :token:`natural`\-th subgoal to prove.
-
-   :n:`[ @ident ]: %{`
-     Focuses on the named goal :token:`ident`.
-
-   .. note::
-
-      Goals are just existential variables and existential variables do not
-      get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`.
-      You may also wrap this in an Ltac-definition like:
-
-      .. coqtop:: in
-
-         Ltac name_goal name := refine ?[name].
-
-   .. seealso:: :ref:`existential-variables`
-
-   .. example::
-
-      This first example uses the Ltac definition above, and the named goals
-      only serve for documentation.
-
-      .. coqtop:: all
-
-         Goal forall n, n + 0 = n.
-         Proof.
-         induction n; [ name_goal base | name_goal step ].
-         [base]: {
-
-      .. coqtop:: all
-
-         reflexivity.
-
-      .. coqtop:: in
-
-         }
-
-      .. coqtop:: all
-
-         [step]: {
-
-      .. coqtop:: all
-
-         simpl.
-         f_equal.
-         assumption.
-         }
-         Qed.
-
-      This can also be a way of focusing on a shelved goal, for instance:
-
-      .. coqtop:: all
-
-         Goal exists n : nat, n = n.
-         eexists ?[x].
-         reflexivity.
-         [x]: exact 0.
-         Qed.
-
-   .. exn:: This proof is focused, but cannot be unfocused this way.
-
-      You are trying to use ``}`` but the current subproof has not been fully solved.
-
-   .. exn:: No such goal (@natural).
-      :undocumented:
-
-   .. exn:: No such goal (@ident).
-      :undocumented:
-
-   .. exn:: Brackets do not support multi-goal selectors.
-
-      Brackets are used to focus on a single goal given either by its position
-      or by its name if it has one.
-
-  .. seealso:: The error messages for bullets below.
-
-.. _bullets:
-
-Bullets
-```````
-
-Alternatively, proofs can be structured with bullets instead of ``{`` and ``}``. The
-use of a bullet ``b`` for the first time focuses on the first goal ``g``, the
-same bullet cannot be used again until the proof of ``g`` is completed,
-then it is mandatory to focus the next goal with ``b``. The consequence is
-that ``g`` and all goals present when ``g`` was focused are focused with the
-same bullet ``b``. See the example below.
-
-Different bullets can be used to nest levels. The scope of bullet does
-not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
-nesting levels provided they are delimited by these. Bullets are made of
-repeated ``-``, ``+`` or ``*`` symbols:
-
-.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } }
-
-Note again that when a focused goal is proved a message is displayed
-together with a suggestion about the right bullet or ``}`` to unfocus it
-or focus the next one.
-
-.. note::
-
-   In Proof General (``Emacs`` interface to |Coq|), you must use
-   bullets with the priority ordering shown above to have a correct
-   indentation. For example ``-`` must be the outer bullet and ``**`` the inner
-   one in the example below.
-
-The following example script illustrates all these features:
-
-.. example::
-
-  .. coqtop:: all
-
-    Goal (((True /\ True) /\ True) /\ True) /\ True.
-    Proof.
-    split.
-    - split.
-    + split.
-    ** { split.
-    - trivial.
-    - trivial.
-    }
-    ** trivial.
-    + trivial.
-    - assert True.
-    { trivial. }
-    assumption.
-    Qed.
-
-.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished.
-
-   Before using bullet :n:`@bullet__1` again, you should first finish proving
-   the current focused goal.
-   Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same.
-
-.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here.
-
-   You must put :n:`@bullet__2` to focus on the next goal. No other bullet is
-   allowed here.
-
-.. exn:: No such goal. Focus next goal with bullet @bullet.
-
-   You tried to apply a tactic but no goals were under focus.
-   Using :n:`@bullet` is  mandatory here.
-
-.. FIXME: the :noindex: below works around a Sphinx issue.
-   (https://github.com/sphinx-doc/sphinx/issues/4979)
-   It should be removed once that issue is fixed.
-
-.. exn:: No such goal. Try unfocusing with %}.
-   :noindex:
-
-   You just finished a goal focused by ``{``, you must unfocus it with ``}``.
-
-Mandatory Bullets
-`````````````````
-
-Using :opt:`Default Goal Selector` with the ``!`` selector forces
-tactic scripts to keep focus to exactly one goal (e.g. using bullets)
-or use explicit goal selectors.
-
-Set Bullet Behavior
-```````````````````
-.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" }
-   :name: Bullet Behavior
-
-   This option controls the bullet behavior and can take two possible values:
-
-   - "None": this makes bullets inactive.
-   - "Strict Subproofs": this makes bullets active (this is the default behavior).
-
-.. _requestinginformation:
-
-Requesting information
-----------------------
-
-
-.. cmd:: Show {? {| @ident | @natural } }
-
-   Displays the current goals.
-
-   :n:`@natural`
-     Display only the :token:`natural`\-th subgoal.
-
-   :n:`@ident`
-     Displays the named goal :token:`ident`. This is useful in
-     particular to display a shelved goal but only works if the
-     corresponding existential variable has been named by the user
-     (see :ref:`existential-variables`) as in the following example.
-
-     .. example::
-
-        .. coqtop:: all abort
-
-           Goal exists n, n = 0.
-           eexists ?[n].
-           Show n.
-
-   .. exn:: No focused proof.
-      :undocumented:
-
-   .. exn:: No such goal.
-      :undocumented:
-
-.. cmd:: Show Proof {? Diffs {? removed } }
-
-   Displays the proof term generated by the tactics
-   that have been applied so far. If the proof is incomplete, the term
-   will contain holes, which correspond to subterms which are still to be
-   constructed. Each hole is an existential variable, which appears as a
-   question mark followed by an identifier.
-
-   Specifying “Diffs” highlights the difference between the
-   current and previous proof step.  By default, the command shows the
-   output once with additions highlighted.  Including “removed” shows
-   the output twice: once showing removals and once showing additions.
-   It does not examine the :opt:`Diffs` option.  See :ref:`showing_proof_diffs`.
-
-.. cmd:: Show Conjectures
-
-   Prints the names of all the
-   theorems that are currently being proved. As it is possible to start
-   proving a previous lemma during the proof of a theorem, there may
-   be multiple names.
-
-.. cmd:: Show Intro
-
-   If the current goal begins by at least one product,
-   prints the name of the first product as it would be
-   generated by an anonymous :tacn:`intro`. The aim of this command is to ease
-   the writing of more robust scripts. For example, with an appropriate
-   Proof General macro, it is possible to transform any anonymous :tacn:`intro`
-   into a qualified one such as ``intro y13``. In the case of a non-product
-   goal, it prints nothing.
-
-.. cmd:: Show Intros
-
-   Similar to the previous command.
-   Simulates the naming process of :tacn:`intros`.
-
-.. cmd:: Show Existentials
-
-   Displays all open goals / existential variables in the current proof
-   along with the type and the context of each variable.
-
-.. cmd:: Show Match @qualid
-
-   Displays a template of the Gallina :token:`match<term_match>`
-   construct with a branch for each constructor of the type
-   :token:`qualid`.  This is used internally by
-   `company-coq <https://github.com/cpitclaudel/company-coq>`_.
-
-   .. example::
-
-      .. coqtop:: all
-
-         Show Match nat.
-
-   .. exn:: Unknown inductive type.
-      :undocumented:
-
-.. cmd:: Show Universes
-
-   Displays the set of all universe constraints and
-   its normalized form at the current stage of the proof, useful for
-   debugging universe inconsistencies.
-
-.. cmd:: Show Goal @natural at @natural
-
-   Available in coqtop.  Displays a goal at a
-   proof state using the goal ID number and the proof state ID number.
-   It is primarily for use by tools such as Prooftree that need to fetch
-   goal history in this way.  Prooftree is a tool for visualizing a proof
-   as a tree that runs in Proof General.
-
-.. cmd:: Guarded
-
-   Some tactics (e.g. :tacn:`refine`) allow to build proofs using
-   fixpoint or co-fixpoint constructions. Due to the incremental nature
-   of interactive proof construction, the check of the termination (or
-   guardedness) of the recursive calls in the fixpoint or cofixpoint
-   constructions is postponed to the time of the completion of the proof.
-
-   The command :cmd:`Guarded` allows checking if the guard condition for
-   fixpoint and cofixpoint is violated at some time of the construction
-   of the proof without having to wait the completion of the proof.
-
-.. _showing_diffs:
-
-Showing differences between proof steps
----------------------------------------
-
-|Coq| can automatically highlight the differences between successive proof steps
-and between values in some error messages.  |Coq| can also highlight differences
-in the proof term.
-For example, the following screenshots of |CoqIDE| and coqtop show the application
-of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
-The conclusion is entirely in pale green because although it’s changed, no tokens were added
-to it.  The second screenshot uses the "removed" option, so it shows the conclusion a
-second time with the old text, with deletions marked in red.  Also, since the hypotheses are
-new, no line of old text is shown for them.
-
-.. comment screenshot produced with:
-   Inductive ev : nat -> Prop :=
-   | ev_0 : ev 0
-   | ev_SS : forall n : nat, ev n -> ev (S (S n)).
-
-   Fixpoint double (n:nat) :=
-     match n with
-     | O => O
-     | S n' => S (S (double n'))
-     end.
-
-   Goal forall n, ev n -> exists k, n = double k.
-   intros n E.
-
-..
-
-  .. image:: ../_static/diffs-coqide-on.png
-     :alt: |CoqIDE| with Set Diffs on
-
-..
-
-  .. image:: ../_static/diffs-coqide-removed.png
-     :alt: |CoqIDE| with Set Diffs removed
-
-..
-
-  .. image:: ../_static/diffs-coqtop-on3.png
-     :alt: coqtop with Set Diffs on
-
-This image shows an error message with diff highlighting in |CoqIDE|:
-
-..
-
-  .. image:: ../_static/diffs-error-message.png
-     :alt: |CoqIDE| error message with diffs
-
-How to enable diffs
-```````````````````
-
-.. opt:: Diffs {| "on" | "off" | "removed" }
-   :name: Diffs
-
-   The “on” setting highlights added tokens in green, while the “removed” setting
-   additionally reprints items with removed tokens in red.  Unchanged tokens in
-   modified items are shown with pale green or red.  Diffs in error messages
-   use red and green for the compared values; they appear regardless of the setting.
-   (Colors are user-configurable.)
-
-For coqtop, showing diffs can be enabled when starting coqtop with the
-``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
-within |Coq|.  You will need to provide the ``-color on|auto`` command-line option when
-you start coqtop in either case.
-
-Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
-variable.  See section :ref:`customization-by-environment-variables`.  Diffs
-use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``.
-
-In |CoqIDE|, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
-command in |CoqIDE|.  You can change the background colors shown for diffs from the
-``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``,
-``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags.  This panel also
-lets you control other attributes of the highlights, such as the foreground
-color, bold, italic, underline and strikeout.
-
-Proof General can also display |Coq|-generated proof diffs automatically.
-Please see the PG documentation section
-"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
-for details.
-
-How diffs are calculated
-````````````````````````
-
-Diffs are calculated as follows:
-
-1. Select the old proof state to compare to, which is the proof state before
-   the last tactic that changed the proof.  Changes that only affect the view
-   of the proof, such as ``all: swap 1 2``, are ignored.
-
-2. For each goal in the new proof state, determine what old goal to compare
-   it to—the one it is derived from or is the same as.  Match the hypotheses by
-   name (order is ignored), handling compacted items specially.
-
-3. For each hypothesis and conclusion (the “items”) in each goal, pass
-   them as strings to the lexer to break them into tokens.  Then apply the
-   Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting.
-
-Notes:
-
-* Aside from the highlights, output for the "on" option should be identical
-  to the undiffed output.
-* Goals completed in the last proof step will not be shown even with the
-  "removed" setting.
-
-.. comment The following screenshots show diffs working with multiple goals and with compacted
-   hypotheses.  In the first one, notice that the goal ``P 1`` is not highlighted at
-   all after the split because it has not changed.
-
-    .. todo: Use this script and remove the screenshots when COQ_COLORS
-      works for coqtop in sphinx
-    .. coqtop:: none
-
-      Set Diffs "on".
-      Parameter P : nat -> Prop.
-      Goal P 1 /\ P 2 /\ P 3.
-
-    .. coqtop:: out
-
-      split.
-
-    .. coqtop:: all abort
-
-      2: split.
-
-  ..
-
-    .. coqtop:: none
-
-      Set Diffs "on".
-      Goal forall n m : nat, n + m = m + n.
-      Set Diffs "on".
-
-    .. coqtop:: out
-
-       intros n.
-
-    .. coqtop:: all abort
-
-      intros m.
-
-This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal
-with 2 goals.  Notice that the goal ``P 1`` is not highlighted at all after
-the split because it has not changed.
-
-..
-
-  .. image:: ../_static/diffs-coqide-multigoal.png
-     :alt: coqide with Set Diffs on with multiple goals
-
-Diffs may appear like this after applying a :tacn:`intro` tactic that results
-in a compacted hypotheses:
-
-..
-
-  .. image:: ../_static/diffs-coqide-compacted.png
-     :alt: coqide with Set Diffs on with compacted hypotheses
-
-.. _showing_proof_diffs:
-
-"Show Proof" differences
-````````````````````````
-
-To show differences in the proof term:
-
-- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command.
-
-- In |CoqIDE|, position the cursor on or just after a tactic to compare the proof term
-  after the tactic with the proof term before the tactic, then select
-  `View / Show Proof` from the menu or enter the associated key binding.
-  Differences will be shown applying the current `Show Diffs` setting
-  from the `View` menu.  If the current setting is `Don't show diffs`, diffs
-  will not be shown.
-
-  Output with the "added and removed" option looks like this:
-
-  ..
-
-    .. image:: ../_static/diffs-show-proof.png
-       :alt: coqide with Set Diffs on with compacted hypotheses
-
-Controlling the effect of proof editing commands
-------------------------------------------------
-
-
-.. opt:: Hyps Limit @natural
-   :name: Hyps Limit
-
-   This option controls the maximum number of hypotheses displayed in goals
-   after the application of a tactic. All the hypotheses remain usable
-   in the proof development.
-   When unset, it goes back to the default mode which is to print all
-   available hypotheses.
-
-
-.. flag:: Nested Proofs Allowed
-
-   When turned on (it is off by default), this flag enables support for nested
-   proofs: a new assertion command can be inserted before the current proof is
-   finished, in which case |Coq| will temporarily switch to the proof of this
-   *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
-   or :cmd:`Defined`), its statement will be made available (as if it had been
-   proved before starting the previous proof) and |Coq| will switch back to the
-   proof of the previous assertion.
-
-.. flag:: Printing Goal Names
-
-   When turned on, the name of the goal is printed in interactive
-   proof mode, which can be useful in cases of cross references
-   between goals.
-
-Controlling memory usage
-------------------------
-
-.. cmd:: Print Debug GC
-
-   Prints heap usage statistics, which are values from the `stat` type of the `Gc` module
-   described
-   `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_
-   in the |OCaml| documentation.
-   The `live_words`, `heap_words` and `top_heap_words` values give the basic information.
-   Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables.
-
-When experiencing high memory usage the following commands can be used
-to force |Coq| to optimize some of its internal data structures.
-
-.. cmd:: Optimize Proof
-
-   Shrink the data structure used to represent the current proof.
-
-
-.. cmd:: Optimize Heap
-
-   Perform a heap compaction.  This is generally an expensive operation.
-   See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-   There is also an analogous tactic :tacn:`optimize_heap`.
-
-Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>`
-environment variable.
diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
index 8e9990c45f..51aebd5661 100644
--- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst
+++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst
@@ -1,3 +1,576 @@
+.. _proofhandling:
+
+-------------------
+ Proof handling
+-------------------
+
+In |Coq|’s proof editing mode all top-level commands documented in
+Chapter :ref:`vernacularcommands` remain available and the user has access to specialized
+commands dealing with proof development pragmas documented in this
+section. They can also use some other specialized commands called
+*tactics*. They are the very tools allowing the user to deal with
+logical reasoning. They are documented in Chapter :ref:`tactics`.
+
+|Coq| user interfaces usually have a way of marking whether the user has
+switched to proof editing mode. For instance, in coqtop the prompt ``Coq <``   is changed into
+:n:`@ident <`   where :token:`ident` is the declared name of the theorem currently edited.
+
+At each stage of a proof development, one has a list of goals to
+prove. Initially, the list consists only in the theorem itself. After
+having applied some tactics, the list of goals contains the subgoals
+generated by the tactics.
+
+To each subgoal is associated a number of hypotheses called the *local context*
+of the goal. Initially, the local context contains the local variables and
+hypotheses of the current section (see Section :ref:`gallina-assumptions`) and
+the local variables and hypotheses of the theorem statement. It is enriched by
+the use of certain tactics (see e.g. :tacn:`intro`).
+
+When a proof is completed, the message ``Proof completed`` is displayed.
+One can then register this proof as a defined constant in the
+environment. Because there exists a correspondence between proofs and
+terms of λ-calculus, known as the *Curry-Howard isomorphism*
+:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those
+terms are called *proof terms*.
+
+
+.. exn:: No focused proof.
+
+   |Coq| raises this error message when one attempts to use a proof editing command
+   out of the proof editing mode.
+
+.. _proof-editing-mode:
+
+Entering and leaving proof editing mode
+---------------------------------------
+
+The proof editing mode is entered by asserting a statement, which typically is
+the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
+list of assertion commands is given in :ref:`Assertions`. The command
+:cmd:`Goal` can also be used.
+
+.. cmd:: Goal @type
+
+   This is intended for quick assertion of statements, without knowing in
+   advance which name to give to the assertion, typically for quick
+   testing of the provability of a statement. If the proof of the
+   statement is eventually completed and validated, the statement is then
+   bound to the name ``Unnamed_thm`` (or a variant of this name not already
+   used for another statement).
+
+.. cmd:: Qed
+
+   This command is available in interactive editing proof mode when the
+   proof is completed. Then :cmd:`Qed` extracts a proof term from the proof
+   script, switches back to |Coq| top-level and attaches the extracted
+   proof term to the declared name of the original goal. The name is
+   added to the environment as an opaque constant.
+
+   .. exn:: Attempt to save an incomplete proof.
+      :undocumented:
+
+   .. note::
+
+      Sometimes an error occurs when building the proof term, because
+      tactics do not enforce completely the term construction
+      constraints.
+
+      The user should also be aware of the fact that since the
+      proof term is completely rechecked at this point, one may have to wait
+      a while when the proof is large. In some exceptional cases one may
+      even incur a memory overflow.
+
+.. cmd:: Save @ident
+   :name: Save
+
+   Saves a completed proof with the name :token:`ident`, which
+   overrides any name provided by the :cmd:`Theorem` command or
+   its variants.
+
+.. cmd:: Defined {? @ident }
+
+   Similar to :cmd:`Qed` and :cmd:`Save`, except the proof is made *transparent*, which means
+   that its content can be explicitly used for type checking and that it can be
+   unfolded in conversion tactics (see :ref:`performingcomputations`,
+   :cmd:`Opaque`, :cmd:`Transparent`).  If :token:`ident` is specified,
+   the proof is defined with the given name, which overrides any name
+   provided by the :cmd:`Theorem` command or its variants.
+
+.. cmd:: Admitted
+
+   This command is available in interactive editing mode to give up
+   the current proof and declare the initial goal as an axiom.
+
+.. cmd:: Abort {? {| All | @ident } }
+
+   Cancels the current proof development, switching back to
+   the previous proof development, or to the |Coq| toplevel if no other
+   proof was being edited.
+
+   :n:`@ident`
+     Aborts editing the proof named :n:`@ident` for use when you have
+     nested proofs.  See also :flag:`Nested Proofs Allowed`.
+
+   :n:`All`
+     Aborts all current proofs.
+
+   .. exn:: No focused proof (No proof-editing in progress).
+      :undocumented:
+
+.. cmd:: Proof @term
+   :name: Proof `term`
+
+   This command applies in proof editing mode. It is equivalent to
+   :n:`exact @term. Qed.`
+   That is, you have to give the full proof in one gulp, as a
+   proof term (see Section :ref:`applyingtheorems`).
+
+   .. warning::
+
+      Use of this command is discouraged.  In particular, it
+      doesn't work in Proof General because it must
+      immediately follow the command that opened proof mode, but
+      Proof General inserts :cmd:`Unset` :flag:`Silent` before it (see
+      `Proof General issue #498
+      <https://github.com/ProofGeneral/PG/issues/498>`_).
+
+.. cmd:: Proof
+
+   Is a no-op which is useful to delimit the sequence of tactic commands
+   which start a proof, after a :cmd:`Theorem` command. It is a good practice to
+   use :cmd:`Proof` as an opening parenthesis, closed in the script with a
+   closing :cmd:`Qed`.
+
+   .. seealso:: :cmd:`Proof with`
+
+.. cmd:: Proof using @section_var_expr {? with @ltac_expr }
+
+   .. insertprodn section_var_expr starred_ident_ref
+
+   .. prodn::
+      section_var_expr ::= {* @starred_ident_ref }
+      | {? - } @section_var_expr50
+      section_var_expr50 ::= @section_var_expr0 - @section_var_expr0
+      | @section_var_expr0 + @section_var_expr0
+      | @section_var_expr0
+      section_var_expr0 ::= @starred_ident_ref
+      | ( @section_var_expr ) {? * }
+      starred_ident_ref ::= @ident {? * }
+      | Type {? * }
+      | All
+
+   Opens proof editing mode, declaring the set of
+   section variables (see :ref:`gallina-assumptions`) used by the proof.
+   At :cmd:`Qed` time, the
+   system verifies that the set of section variables used in
+   the proof is a subset of the declared one.
+
+   The set of declared variables is closed under type dependency. For
+   example, if ``T`` is a variable and ``a`` is a variable of type
+   ``T``, then the commands ``Proof using a`` and ``Proof using T a``
+   are equivalent.
+
+   The set of declared variables always includes the variables used by
+   the statement. In other words ``Proof using e`` is equivalent to
+   ``Proof using Type + e`` for any declaration expression ``e``.
+
+   :n:`- @section_var_expr50`
+     Use all section variables except those specified by :n:`@section_var_expr50`
+
+   :n:`@section_var_expr0 + @section_var_expr0`
+     Use section variables from the union of both collections.
+     See :ref:`nameaset` to see how to form a named collection.
+
+   :n:`@section_var_expr0 - @section_var_expr0`
+     Use section variables which are in the first collection but not in the
+     second one.
+
+   :n:`{? * }`
+     Use the transitive closure of the specified collection.
+
+   :n:`Type`
+     Use only section variables occurring in the statement.  Specifying :n:`*`
+     uses the forward transitive closure of all the section variables occurring
+     in the statement. For example, if the variable ``H`` has type ``p < 5`` then
+     ``H`` is in ``p*`` since ``p`` occurs in the type of ``H``.
+
+   :n:`All`
+     Use all section variables.
+
+   .. seealso:: :ref:`tactics-implicit-automation`
+
+.. attr:: using
+
+   This attribute can be applied to the :cmd:`Definition`, :cmd:`Example`,
+   :cmd:`Fixpoint` and :cmd:`CoFixpoint` commands as well as to :cmd:`Lemma` and
+   its variants.  It takes
+   a :n:`@section_var_expr`, in quotes, as its value. This is equivalent to
+   specifying the same :n:`@section_var_expr` in
+   :cmd:`Proof using`.
+
+   .. example::
+
+      .. coqtop:: all
+
+         Section Test.
+         Variable n : nat.
+         Hypothesis Hn : n <> 0.
+
+         #[using="Hn"]
+         Lemma example : 0 < n.
+
+      .. coqtop:: in
+
+         Abort.
+         End Test.
+
+
+Proof using options
+```````````````````
+
+The following options modify the behavior of ``Proof using``.
+
+
+.. opt:: Default Proof Using "@section_var_expr"
+   :name: Default Proof Using
+
+   Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default
+   Proof Using "a b"`` will complete all ``Proof`` commands not followed by a
+   ``using`` part with ``using a b``.
+
+
+.. flag:: Suggest Proof Using
+
+   When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not
+   provide one.
+
+..  _`nameaset`:
+
+Name a set of section hypotheses for ``Proof using``
+````````````````````````````````````````````````````
+
+.. cmd:: Collection @ident := @section_var_expr
+
+   This can be used to name a set of section
+   hypotheses, with the purpose of making ``Proof using`` annotations more
+   compact.
+
+   .. example::
+
+      Define the collection named ``Some`` containing ``x``, ``y`` and ``z``::
+
+         Collection Some := x y z.
+
+      Define the collection named ``Fewer`` containing only ``x`` and ``y``::
+
+         Collection Fewer := Some - z
+
+      Define the collection named ``Many`` containing the set union or set
+      difference of ``Fewer`` and ``Some``::
+
+         Collection Many := Fewer + Some
+         Collection Many := Fewer - Some
+
+      Define the collection named ``Many`` containing the set difference of
+      ``Fewer`` and the unnamed collection ``x y``::
+
+         Collection Many := Fewer - (x y)
+
+
+
+.. cmd:: Existential @natural {? : @type } := @term
+
+   This command instantiates an existential variable. :token:`natural` is an index in
+   the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`.
+
+   This command is intended to be used to instantiate existential
+   variables when the proof is completed but some uninstantiated
+   existential variables remain. To instantiate existential variables
+   during proof edition, you should use the tactic :tacn:`instantiate`.
+
+.. cmd:: Grab Existential Variables
+
+   This command can be run when a proof has no more goal to be solved but
+   has remaining uninstantiated existential variables. It takes every
+   uninstantiated existential variable and turns it into a goal.
+
+Proof modes
+```````````
+
+When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`,
+|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes
+shipped in the standard |Coq| installation, and furthermore some plugins define
+their own proof modes. The default proof mode used when opening a proof can
+be changed using the following option.
+
+.. opt:: Default Proof Mode @string
+
+   Select the proof mode to use when starting a proof. Depending on the proof
+   mode, various syntactic constructs are allowed when writing an interactive
+   proof. All proof modes support vernacular commands; the proof mode determines
+   which tactic language and set of tactic definitions are available.  The
+   possible option values are:
+
+   `"Classic"`
+     Activates the |Ltac| language and the tactics with the syntax documented
+     in this manual.
+     Some tactics are not available until the associated plugin is loaded,
+     such as `SSR` or `micromega`.
+     This proof mode is set when the :term:`prelude` is loaded.
+
+   `"Noedit"`
+     No tactic
+     language is activated at all. This is the default when the :term:`prelude`
+     is not loaded, e.g. through the `-noinit` option for `coqc`.
+
+   `"Ltac2"`
+     Activates the Ltac2 language and the Ltac2-specific variants of the documented
+     tactics.
+     This value is only available after :cmd:`Requiring <Require>` Ltac2.
+     :cmd:`Importing <Import>` Ltac2 sets this mode.
+
+   Some external plugins also define their own proof mode, which can be
+   activated with this command.
+
+Navigation in the proof tree
+--------------------------------
+
+.. cmd:: Undo {? {? To } @natural }
+
+   Cancels the effect of the last :token:`natural` commands or tactics.
+   The :n:`To @natural` form goes back to the specified state number.
+   If :token:`natural` is not specified, the command goes back one command or tactic.
+
+.. cmd:: Restart
+
+   Restores the proof editing process to the original goal.
+
+   .. exn:: No focused proof to restart.
+      :undocumented:
+
+.. cmd:: Focus {? @natural }
+
+   Focuses the attention on the first subgoal to prove or, if :token:`natural` is
+   specified, the :token:`natural`\-th.  The
+   printing of the other subgoals is suspended until the focused subgoal
+   is solved or unfocused.
+
+   .. deprecated:: 8.8
+
+      Prefer the use of bullets or focusing brackets with a goal selector (see below).
+
+.. cmd:: Unfocus
+
+   This command restores to focus the goal that were suspended by the
+   last :cmd:`Focus` command.
+
+   .. deprecated:: 8.8
+
+.. cmd:: Unfocused
+
+   Succeeds if the proof is fully unfocused, fails if there are some
+   goals out of focus.
+
+.. _curly-braces:
+
+.. index:: {
+           }
+
+.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket,
+   hence the verbose names
+
+.. tacn:: {? {| @natural | [ @ident ] } : } %{
+         %}
+
+   .. todo
+      See https://github.com/coq/coq/issues/12004 and
+      https://github.com/coq/coq/issues/12825.
+
+   ``{`` (without a terminating period) focuses on the first
+   goal.  The subproof can only be
+   unfocused when it has been fully solved (*i.e.*, when there is no
+   focused goal left). Unfocusing is then handled by ``}`` (again, without a
+   terminating period). See also an example in the next section.
+
+   Note that when a focused goal is proved a message is displayed
+   together with a suggestion about the right bullet or ``}`` to unfocus it
+   or focus the next one.
+
+   :n:`@natural:`
+     Focuses on the :token:`natural`\-th subgoal to prove.
+
+   :n:`[ @ident ]: %{`
+     Focuses on the named goal :token:`ident`.
+
+   .. note::
+
+      Goals are just existential variables and existential variables do not
+      get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`.
+      You may also wrap this in an Ltac-definition like:
+
+      .. coqtop:: in
+
+         Ltac name_goal name := refine ?[name].
+
+   .. seealso:: :ref:`existential-variables`
+
+   .. example::
+
+      This first example uses the Ltac definition above, and the named goals
+      only serve for documentation.
+
+      .. coqtop:: all
+
+         Goal forall n, n + 0 = n.
+         Proof.
+         induction n; [ name_goal base | name_goal step ].
+         [base]: {
+
+      .. coqtop:: all
+
+         reflexivity.
+
+      .. coqtop:: in
+
+         }
+
+      .. coqtop:: all
+
+         [step]: {
+
+      .. coqtop:: all
+
+         simpl.
+         f_equal.
+         assumption.
+         }
+         Qed.
+
+      This can also be a way of focusing on a shelved goal, for instance:
+
+      .. coqtop:: all
+
+         Goal exists n : nat, n = n.
+         eexists ?[x].
+         reflexivity.
+         [x]: exact 0.
+         Qed.
+
+   .. exn:: This proof is focused, but cannot be unfocused this way.
+
+      You are trying to use ``}`` but the current subproof has not been fully solved.
+
+   .. exn:: No such goal (@natural).
+      :undocumented:
+
+   .. exn:: No such goal (@ident).
+      :undocumented:
+
+   .. exn:: Brackets do not support multi-goal selectors.
+
+      Brackets are used to focus on a single goal given either by its position
+      or by its name if it has one.
+
+  .. seealso:: The error messages for bullets below.
+
+.. _bullets:
+
+Bullets
+```````
+
+Alternatively, proofs can be structured with bullets instead of ``{`` and ``}``. The
+use of a bullet ``b`` for the first time focuses on the first goal ``g``, the
+same bullet cannot be used again until the proof of ``g`` is completed,
+then it is mandatory to focus the next goal with ``b``. The consequence is
+that ``g`` and all goals present when ``g`` was focused are focused with the
+same bullet ``b``. See the example below.
+
+Different bullets can be used to nest levels. The scope of bullet does
+not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
+nesting levels provided they are delimited by these. Bullets are made of
+repeated ``-``, ``+`` or ``*`` symbols:
+
+.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } }
+
+Note again that when a focused goal is proved a message is displayed
+together with a suggestion about the right bullet or ``}`` to unfocus it
+or focus the next one.
+
+.. note::
+
+   In Proof General (``Emacs`` interface to |Coq|), you must use
+   bullets with the priority ordering shown above to have a correct
+   indentation. For example ``-`` must be the outer bullet and ``**`` the inner
+   one in the example below.
+
+The following example script illustrates all these features:
+
+.. example::
+
+  .. coqtop:: all
+
+    Goal (((True /\ True) /\ True) /\ True) /\ True.
+    Proof.
+    split.
+    - split.
+    + split.
+    ** { split.
+    - trivial.
+    - trivial.
+    }
+    ** trivial.
+    + trivial.
+    - assert True.
+    { trivial. }
+    assumption.
+    Qed.
+
+.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished.
+
+   Before using bullet :n:`@bullet__1` again, you should first finish proving
+   the current focused goal.
+   Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same.
+
+.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here.
+
+   You must put :n:`@bullet__2` to focus on the next goal. No other bullet is
+   allowed here.
+
+.. exn:: No such goal. Focus next goal with bullet @bullet.
+
+   You tried to apply a tactic but no goals were under focus.
+   Using :n:`@bullet` is  mandatory here.
+
+.. FIXME: the :noindex: below works around a Sphinx issue.
+   (https://github.com/sphinx-doc/sphinx/issues/4979)
+   It should be removed once that issue is fixed.
+
+.. exn:: No such goal. Try unfocusing with %}.
+   :noindex:
+
+   You just finished a goal focused by ``{``, you must unfocus it with ``}``.
+
+Mandatory Bullets
+~~~~~~~~~~~~~~~~~
+
+Using :opt:`Default Goal Selector` with the ``!`` selector forces
+tactic scripts to keep focus to exactly one goal (e.g. using bullets)
+or use explicit goal selectors.
+
+Set Bullet Behavior
+~~~~~~~~~~~~~~~~~~~
+
+.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" }
+   :name: Bullet Behavior
+
+   This option controls the bullet behavior and can take two possible values:
+
+   - "None": this makes bullets inactive.
+   - "Strict Subproofs": this makes bullets active (this is the default behavior).
+
+Modifying the order of goals
+````````````````````````````
+
 .. tacn:: cycle @integer
    :name: cycle
 
@@ -56,6 +629,9 @@
          repeat split.
          all: revgoals.
 
+Postponing the proof of some goals
+``````````````````````````````````
+
 .. tacn:: shelve
    :name: shelve
 
@@ -100,3 +676,362 @@
 
    The ``give_up`` tactic can be used while editing a proof, to choose to
    write the proof script in a non-sequential order.
+
+.. _requestinginformation:
+
+Requesting information
+----------------------
+
+
+.. cmd:: Show {? {| @ident | @natural } }
+
+   Displays the current goals.
+
+   :n:`@natural`
+     Display only the :token:`natural`\-th subgoal.
+
+   :n:`@ident`
+     Displays the named goal :token:`ident`. This is useful in
+     particular to display a shelved goal but only works if the
+     corresponding existential variable has been named by the user
+     (see :ref:`existential-variables`) as in the following example.
+
+     .. example::
+
+        .. coqtop:: all abort
+
+           Goal exists n, n = 0.
+           eexists ?[n].
+           Show n.
+
+   .. exn:: No focused proof.
+      :undocumented:
+
+   .. exn:: No such goal.
+      :undocumented:
+
+.. cmd:: Show Proof {? Diffs {? removed } }
+
+   Displays the proof term generated by the tactics
+   that have been applied so far. If the proof is incomplete, the term
+   will contain holes, which correspond to subterms which are still to be
+   constructed. Each hole is an existential variable, which appears as a
+   question mark followed by an identifier.
+
+   Specifying “Diffs” highlights the difference between the
+   current and previous proof step.  By default, the command shows the
+   output once with additions highlighted.  Including “removed” shows
+   the output twice: once showing removals and once showing additions.
+   It does not examine the :opt:`Diffs` option.  See :ref:`showing_proof_diffs`.
+
+.. cmd:: Show Conjectures
+
+   Prints the names of all the
+   theorems that are currently being proved. As it is possible to start
+   proving a previous lemma during the proof of a theorem, there may
+   be multiple names.
+
+.. cmd:: Show Intro
+
+   If the current goal begins by at least one product,
+   prints the name of the first product as it would be
+   generated by an anonymous :tacn:`intro`. The aim of this command is to ease
+   the writing of more robust scripts. For example, with an appropriate
+   Proof General macro, it is possible to transform any anonymous :tacn:`intro`
+   into a qualified one such as ``intro y13``. In the case of a non-product
+   goal, it prints nothing.
+
+.. cmd:: Show Intros
+
+   Similar to the previous command.
+   Simulates the naming process of :tacn:`intros`.
+
+.. cmd:: Show Existentials
+
+   Displays all open goals / existential variables in the current proof
+   along with the type and the context of each variable.
+
+.. cmd:: Show Match @qualid
+
+   Displays a template of the Gallina :token:`match<term_match>`
+   construct with a branch for each constructor of the type
+   :token:`qualid`.  This is used internally by
+   `company-coq <https://github.com/cpitclaudel/company-coq>`_.
+
+   .. example::
+
+      .. coqtop:: all
+
+         Show Match nat.
+
+   .. exn:: Unknown inductive type.
+      :undocumented:
+
+.. cmd:: Show Universes
+
+   Displays the set of all universe constraints and
+   its normalized form at the current stage of the proof, useful for
+   debugging universe inconsistencies.
+
+.. cmd:: Show Goal @natural at @natural
+
+   Available in coqtop.  Displays a goal at a
+   proof state using the goal ID number and the proof state ID number.
+   It is primarily for use by tools such as Prooftree that need to fetch
+   goal history in this way.  Prooftree is a tool for visualizing a proof
+   as a tree that runs in Proof General.
+
+.. cmd:: Guarded
+
+   Some tactics (e.g. :tacn:`refine`) allow to build proofs using
+   fixpoint or co-fixpoint constructions. Due to the incremental nature
+   of interactive proof construction, the check of the termination (or
+   guardedness) of the recursive calls in the fixpoint or cofixpoint
+   constructions is postponed to the time of the completion of the proof.
+
+   The command :cmd:`Guarded` allows checking if the guard condition for
+   fixpoint and cofixpoint is violated at some time of the construction
+   of the proof without having to wait the completion of the proof.
+
+.. _showing_diffs:
+
+Showing differences between proof steps
+---------------------------------------
+
+|Coq| can automatically highlight the differences between successive proof steps
+and between values in some error messages.  |Coq| can also highlight differences
+in the proof term.
+For example, the following screenshots of |CoqIDE| and coqtop show the application
+of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
+The conclusion is entirely in pale green because although it’s changed, no tokens were added
+to it.  The second screenshot uses the "removed" option, so it shows the conclusion a
+second time with the old text, with deletions marked in red.  Also, since the hypotheses are
+new, no line of old text is shown for them.
+
+.. comment screenshot produced with:
+   Inductive ev : nat -> Prop :=
+   | ev_0 : ev 0
+   | ev_SS : forall n : nat, ev n -> ev (S (S n)).
+
+   Fixpoint double (n:nat) :=
+     match n with
+     | O => O
+     | S n' => S (S (double n'))
+     end.
+
+   Goal forall n, ev n -> exists k, n = double k.
+   intros n E.
+
+..
+
+  .. image:: ../_static/diffs-coqide-on.png
+     :alt: |CoqIDE| with Set Diffs on
+
+..
+
+  .. image:: ../_static/diffs-coqide-removed.png
+     :alt: |CoqIDE| with Set Diffs removed
+
+..
+
+  .. image:: ../_static/diffs-coqtop-on3.png
+     :alt: coqtop with Set Diffs on
+
+This image shows an error message with diff highlighting in |CoqIDE|:
+
+..
+
+  .. image:: ../_static/diffs-error-message.png
+     :alt: |CoqIDE| error message with diffs
+
+How to enable diffs
+```````````````````
+
+.. opt:: Diffs {| "on" | "off" | "removed" }
+   :name: Diffs
+
+   The “on” setting highlights added tokens in green, while the “removed” setting
+   additionally reprints items with removed tokens in red.  Unchanged tokens in
+   modified items are shown with pale green or red.  Diffs in error messages
+   use red and green for the compared values; they appear regardless of the setting.
+   (Colors are user-configurable.)
+
+For coqtop, showing diffs can be enabled when starting coqtop with the
+``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
+within |Coq|.  You will need to provide the ``-color on|auto`` command-line option when
+you start coqtop in either case.
+
+Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
+variable.  See section :ref:`customization-by-environment-variables`.  Diffs
+use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``.
+
+In |CoqIDE|, diffs should be enabled from the ``View`` menu.  Don’t use the ``Set Diffs``
+command in |CoqIDE|.  You can change the background colors shown for diffs from the
+``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``,
+``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags.  This panel also
+lets you control other attributes of the highlights, such as the foreground
+color, bold, italic, underline and strikeout.
+
+Proof General can also display |Coq|-generated proof diffs automatically.
+Please see the PG documentation section
+"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_)
+for details.
+
+How diffs are calculated
+````````````````````````
+
+Diffs are calculated as follows:
+
+1. Select the old proof state to compare to, which is the proof state before
+   the last tactic that changed the proof.  Changes that only affect the view
+   of the proof, such as ``all: swap 1 2``, are ignored.
+
+2. For each goal in the new proof state, determine what old goal to compare
+   it to—the one it is derived from or is the same as.  Match the hypotheses by
+   name (order is ignored), handling compacted items specially.
+
+3. For each hypothesis and conclusion (the “items”) in each goal, pass
+   them as strings to the lexer to break them into tokens.  Then apply the
+   Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting.
+
+Notes:
+
+* Aside from the highlights, output for the "on" option should be identical
+  to the undiffed output.
+* Goals completed in the last proof step will not be shown even with the
+  "removed" setting.
+
+.. comment The following screenshots show diffs working with multiple goals and with compacted
+   hypotheses.  In the first one, notice that the goal ``P 1`` is not highlighted at
+   all after the split because it has not changed.
+
+    .. todo: Use this script and remove the screenshots when COQ_COLORS
+      works for coqtop in sphinx
+    .. coqtop:: none
+
+      Set Diffs "on".
+      Parameter P : nat -> Prop.
+      Goal P 1 /\ P 2 /\ P 3.
+
+    .. coqtop:: out
+
+      split.
+
+    .. coqtop:: all abort
+
+      2: split.
+
+  ..
+
+    .. coqtop:: none
+
+      Set Diffs "on".
+      Goal forall n m : nat, n + m = m + n.
+      Set Diffs "on".
+
+    .. coqtop:: out
+
+       intros n.
+
+    .. coqtop:: all abort
+
+      intros m.
+
+This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal
+with 2 goals.  Notice that the goal ``P 1`` is not highlighted at all after
+the split because it has not changed.
+
+..
+
+  .. image:: ../_static/diffs-coqide-multigoal.png
+     :alt: coqide with Set Diffs on with multiple goals
+
+Diffs may appear like this after applying a :tacn:`intro` tactic that results
+in a compacted hypotheses:
+
+..
+
+  .. image:: ../_static/diffs-coqide-compacted.png
+     :alt: coqide with Set Diffs on with compacted hypotheses
+
+.. _showing_proof_diffs:
+
+"Show Proof" differences
+````````````````````````
+
+To show differences in the proof term:
+
+- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command.
+
+- In |CoqIDE|, position the cursor on or just after a tactic to compare the proof term
+  after the tactic with the proof term before the tactic, then select
+  `View / Show Proof` from the menu or enter the associated key binding.
+  Differences will be shown applying the current `Show Diffs` setting
+  from the `View` menu.  If the current setting is `Don't show diffs`, diffs
+  will not be shown.
+
+  Output with the "added and removed" option looks like this:
+
+  ..
+
+    .. image:: ../_static/diffs-show-proof.png
+       :alt: coqide with Set Diffs on with compacted hypotheses
+
+Controlling the effect of proof editing commands
+------------------------------------------------
+
+
+.. opt:: Hyps Limit @natural
+   :name: Hyps Limit
+
+   This option controls the maximum number of hypotheses displayed in goals
+   after the application of a tactic. All the hypotheses remain usable
+   in the proof development.
+   When unset, it goes back to the default mode which is to print all
+   available hypotheses.
+
+
+.. flag:: Nested Proofs Allowed
+
+   When turned on (it is off by default), this flag enables support for nested
+   proofs: a new assertion command can be inserted before the current proof is
+   finished, in which case |Coq| will temporarily switch to the proof of this
+   *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
+   or :cmd:`Defined`), its statement will be made available (as if it had been
+   proved before starting the previous proof) and |Coq| will switch back to the
+   proof of the previous assertion.
+
+.. flag:: Printing Goal Names
+
+   When turned on, the name of the goal is printed in interactive
+   proof mode, which can be useful in cases of cross references
+   between goals.
+
+Controlling memory usage
+------------------------
+
+.. cmd:: Print Debug GC
+
+   Prints heap usage statistics, which are values from the `stat` type of the `Gc` module
+   described
+   `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_
+   in the |OCaml| documentation.
+   The `live_words`, `heap_words` and `top_heap_words` values give the basic information.
+   Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables.
+
+When experiencing high memory usage the following commands can be used
+to force |Coq| to optimize some of its internal data structures.
+
+.. cmd:: Optimize Proof
+
+   Shrink the data structure used to represent the current proof.
+
+
+.. cmd:: Optimize Heap
+
+   Perform a heap compaction.  This is generally an expensive operation.
+   See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
+   There is also an analogous tactic :tacn:`optimize_heap`.
+
+Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>`
+environment variable.