3 files changed, 44 insertions, 1 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index dd80b29bda..b722b1af74 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -940,6 +940,13 @@ below will fail immediately and won't print anything.
 In any case, the value returned by the fully applied quotation is an
 unspecified dummy Ltac1 closure and should not be further used.
 
+Switching between Ltac languages
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We recommend using the :opt:`Default Proof Mode` option to switch between tactic
+languages with a proof-based granularity. This allows to incrementally port
+the proof scripts.
+
 Transition from Ltac1
 ---------------------
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 6884b6e998..b1734b3f19 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -265,6 +265,35 @@ Name a set of section hypotheses for ``Proof using``
    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
+   :name: Default Proof Mode
+
+   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. The possible option values are listed below.
+
+   - "Classic": this is the default. It activates the |Ltac| language to interact
+     with the proof, and also allows vernacular commands.
+
+   - "Noedit": this proof mode only allows vernacular commands. No tactic
+     language is activated at all. This is the default when the prelude is not
+     loaded, e.g. through the `-noinit` option for `coqc`.
+
+   - "Ltac2": this proof mode is made available when requiring the Ltac2
+     library, and is set to be the default when it is imported. It allows
+     to use the Ltac2 language, as well as vernacular commands.
+
+   - Some external plugins also define their own proof mode, which can be
+     activated via this command.
 
 Navigation in the proof tree
 --------------------------------
@@ -490,6 +519,13 @@ The following example script illustrates all these features:
 
    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" }
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 89b24ea8a3..a38c26c2b3 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1200,7 +1200,7 @@ Controlling the locality of commands
    + Commands whose default behavior is to extend their effect outside
      sections but not outside modules when they occur in a section and to
      extend their effect outside the module or library file they occur in
-     when no section contains them.For these commands, the Local modifier
+     when no section contains them. For these commands, the Local modifier
      limits the effect to the current section or module while the Global
      modifier extends the effect outside the module even when the command
      occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this