Document the Set Default Proof Mode command.

Fixes #10909: Set Default Proof Mode is not documented.

2 files changed, 36 insertions, 0 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 0527e26353..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
 --------------------------------