[nongnu] elpa/proof-general f5600a16d9: fix(ProofGeneral.texi): s/.dir-local.el/.dir-locals.el/; Add idx items

[ELPA Syncer]

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

    fix(ProofGeneral.texi): s/.dir-local.el/.dir-locals.el/; Add idx items
---
 doc/ProofGeneral.texi | 33 ++++++++++++++++++++++++++++-----
 1 file changed, 28 insertions(+), 5 deletions(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 2435ebfab6..bdcb0985d5 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -82,6 +82,19 @@
 @c merge functions into variables index
 @c @syncodeindex fn vr
 
+@c Attempt before 
https://github.com/ProofGeneral/proofgeneral.github.io/commit/dbd891d01fd37564cb329543b8e48cfe9a3e6d7f
+@c @macro emacsuorinforef {txt,sectiondash,sectionspace}
+@c @iftex
+@c 
@uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/\sectiondash\#\sectiondash\,\txt\}
+@c @end iftex
+@c @ifhtml
+@c 
@uref{https://www.gnu.org/software/emacs/manual/html_node/emacs/\sectiondash\#\sectiondash\,\txt\}
+@c @end ifhtml
+@c @ifinfo
+@c @inforef{\sectionspace\, ,emacs}
+@c @end ifinfo
+@c @end macro
+
 @finalout
 @titlepage
 @title Proof General
@@ -4251,6 +4264,7 @@ Inserts ``End <section-name>.'' (this should work well 
with nested sections).
 
 @node Using the Coq project file
 @section Using the Coq project file
+@cindex _CoqProject
 
 The Coq project file is the recommended way to configure the Coq
 load path and the mapping of logical module names to physical
@@ -4308,6 +4322,7 @@ below.
 
 @node Changing the name of the coq project file
 @subsection Changing the name of the coq project file
+@cindex .dir-locals.el
 
 To change the name of the Coq project file, configure
 @code{coq-project-filename} (select menu @code{Proof-General ->
@@ -4319,18 +4334,18 @@ If you only want to change the name of the Coq project 
file for
 one project you can set the option as local file variable,
 @ref{Using file variables}. This can be done either directly in
 every file or once for all files of a directory tree with a
-@code{.dir-local.el} file, @inforef{Directory Variables, ,emacs}.
-The file @code{.dir-local.el} should then contain
+@code{.dir-locals.el} file, @inforef{Directory Variables, ,emacs}.
+The file @code{.dir-locals.el} should then contain
 
 @lisp
 ((coq-mode . ((coq-project-filename . "myprojectfile"))))
 @end lisp
 
-Note that variables set in @code{.dir-local.el} are automatically
+Note that variables set in @code{.dir-locals.el} are automatically
 made buffer local (such that files in different directories can
 have their independent setting of @code{coq-project-filename}).
 If you make complex customizations using @code{eval} in
-@code{.dir-local.el}, you might want to add appropriate calls to
+@code{.dir-locals.el}, you might want to add appropriate calls to
 @code{make-local-variable}.
 
 Documentation of the user option @code{coq-project-filename}:
@@ -4375,6 +4390,7 @@ on a per project basis.
 
 @node Proof using annotations
 @section Proof using annotations
+@cindex Proof using
 
 In order to process files asynchronously and pre-compile files (.vos and
 .vok files), it is advised (inside sections) to list the section
@@ -4408,6 +4424,7 @@ This can be configured either via Coq menu or by setting 
variable
 
 @node Multiple File Support
 @section Multiple File Support
+@cindex multiple file support
 
 Since version 4.1 Coq Proof General has multiple file support. It
 consists of the following points:
@@ -4597,7 +4614,7 @@ compilation, but exclusively, depending on the Coq 
version,
 
 @node Locking Ancestors
 @subsection Locking Ancestors
-
+@vindex proof-strict-read-only
 
 Locking ancestor files works as a side effect of dependency
 checking. This means that ancestor locking does only work when
@@ -5055,6 +5072,7 @@ General will perform some unnecessary compilations.
 
 @node Omitting proofs for speed
 @section Omitting proofs for speed
+@cindex Omitting proofs for speed
 
 To speed up asserting larger chunks, Proof General can omit
 complete opaque proofs by silently replacing the whole proof
@@ -5278,6 +5296,7 @@ you want to save abbrevs; answer yes.
 
 @node Proof-Tree Visualization
 @section Proof-Tree Visualization
+@cindex Proof-Tree visualization
 
 Starting with Proof General version 4.2 and Coq version 8.4, Coq
 Proof General has full support for proof-tree visualization, 
@@ -5297,6 +5316,9 @@ several layers.
 
 @node Showing Proof Diffs
 @section Showing Proof Diffs
+@cindex Showing Proof Diffs
+@vindex coq-diffs
+@vindex coq-show-proof-stepwise
 
 Coq 8.10 supports automatically highlighting the differences
 between successive proof steps in Proof General.  The feature is described in 
the
@@ -5336,6 +5358,7 @@ with non-@code{Bg} faces.
 
 @node Opam-switch-mode support
 @section Opam-switch-mode support
+@cindex 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