[nongnu] elpa/proof-general a3d0fc9875 2/4: docs: Document OPSW in ProofGeneral.texi

[ELPA Syncer]

branch: elpa/proof-general
commit a3d0fc9875e5d24de52be6685c885a60aca4c05b
Author: Erik Martin-Dorel <erik@martin-dorel.org>
Commit: Erik Martin-Dorel <erik@martin-dorel.org>

    docs: Document OPSW in ProofGeneral.texi
    
    & Run (make -C doc magic)
---
 CHANGES               |  6 +++---
 doc/ProofGeneral.texi | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index e20941ce12..bfce6dcd85 100644
--- a/CHANGES
+++ b/CHANGES
@@ -108,12 +108,12 @@ standard support.
     documentation of this variable for an explanation of the different
     possible values and some more information.
 
-*** Make Proof General/Coq `opam-switch-mode` aware
+*** Make ProofGeneral/Coq `opam-switch-mode' aware
 
     When opam-switch-mode is loaded, the Coq background process can be
     killed when changing the opam switch through opam-switch-mode, see
-    `coq-kill-coq-on-opam-switch` and
-    https://github.com/ProofGeneral/opam-switch-mode.
+    `coq-kill-coq-on-opam-switch' and
+    https://github.com/ProofGeneral/opam-switch-mode
 
 *** Limited extensibility for indentation 
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index f7748846f0..bb51dbb55b 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4187,6 +4187,7 @@ assistant.  It supports most of the generic features of 
Proof General.
 * Holes feature::
 * Proof-Tree Visualization::
 * Showing Proof Diffs::
+* Opam-switch-mode support::
 @end menu
 
 
@@ -5320,6 +5321,41 @@ have added or removed tokens are shown with the entire 
line highlighted with
 a @code{Coq Diffs ... Bg} face.  The added or removed tokens themselves are 
highlighted
 with non-@code{Bg} faces.
 
+@node Opam-switch-mode support
+@section Opam-switch-mode support
+
+Coq can be installed using @code{opam} (the OCaml package manager),
+which makes it easy to manage several different switches, having each
+a different version of Coq.
+
+Instead of running a command like @code{opam switch ...} in a terminal
+and restarting emacs to benefit from a different switch, one can:
+
+@itemize @bullet
+@item
+@b{Install} the
+@uref{https://github.com/ProofGeneral/opam-switch-mode,
+opam-switch-mode} and use the dedicated mode bar menu @code{OPSW} it
+provides.
+@item
+@b{Configure} Proof General using the customization option
+@code{coq-kill-coq-on-opam-switch}, so that the Coq background process
+is killed when changing the opam switch through
+@code{opam-switch-mode}.
+@end itemize
+
+@c TEXI DOCSTRING MAGIC: coq-kill-coq-on-opam-switch
+@defvar coq-kill-coq-on-opam-switch 
+If t kill coq when the opam switch changes (requires 
@samp{opam-switch-mode}).@*
+When @samp{opam-switch-mode} is loaded and the user changes the opam switch
+through @samp{opam-switch-mode} then this option controls whether the coq
+background process (the proof shell) is killed such that the next
+assert command starts a new proof shell, probably using a
+different coq version from a different opam switch.
+
+See https://github.com/ProofGeneral/opam-switch-mode for 
@samp{opam-switch-mode}
+@end defvar
+
 @c =================================================================
 @c
 @c  CHAPTER: EasyCrypt Proof General