Add documentation about the recommended way to set coq-prog-name.

2 files changed, 40 insertions, 3 deletions

diff --git a/FAQ b/FAQ
index 0c616a51..0bc70b05 100644
--- a/FAQ
+++ b/FAQ
@@ -8,6 +8,24 @@ Please also check the BUGS file.
 
 -----------------------------------------------------------------
 
+Q. I use ProofGeneral with custom installations of Coq, depending
+   on the project I am working on. How can I change coq-prog-name
+   accordingly?
+
+A. The recommended way to set coq-prog-name is to create a file
+   .dir-locals.el in the top-level folder of your Coq project (or
+   if applicable, in the sub-folder containing the Coq source files)
+   with content:
+
+      ((coq-mode . ((coq-prog-name . ".../path/to/coqtop"))))
+
+   Then restart Emacs
+   (or just run: M-x proof-shell-exit RET yes RET, M-x normal-mode RET
+   in the Coq buffer before restarting the Coq process) in order
+   to take this change into account.
+
+-----------------------------------------------------------------
+
 Q. The prover process produces some useful output I'd like to
    keep a note of, how do I do that?
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index bd5e591f..7c62debd 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4028,11 +4028,17 @@ when a file is loaded. File variables and their values
 are written as a list at the end of
 the file.
 
-@emph{Remarque 1:} The examples in the following are for Coq but the
+@emph{Remark 1:} The examples in the following are for Coq but the
 trick is applicable to other provers. 
 
-@emph{Remarque 2:} For Coq specifically there is a recommended other way
-of configuring coq options: project files (@ref{Using the Coq project file}).
+@emph{Remark 2:} For Coq specifically, there is a recommended other way
+of configuring Coq options:
+project files (@ref{Using the Coq project file}).
+Actually, project files are intended to be included in the
+distribution of a library (and included in its repository), so the Coq
+options specified in project files are supposed to work for all users.
+In contrast, user-defined options such as @code{coq-prog-name} should
+preferably be specified in a directory-local-variables file (see below).
 
 For example, in Coq projects involving multiple directories, it is necessary
 to set the variable @code{coq-load-path} 
@@ -4098,6 +4104,19 @@ The value in this file must be an alist that maps mode names to alists,
 where these latter alists map variables to values. You can aso put
 arbitrary code in this file @inforef{Directory Variables, ,emacs}.
 
+Regarding the configuration of the @code{coq-prog-name} variable, the
+@code{.dir-locals.el} file should contain something like:
+
+@lisp
+((coq-mode . ((coq-prog-name . ".../path/to/coqtop"))))
+@end lisp
+
+@emph{Note:} if you add such content to the @code{.dir-locals.el} file
+you should restart Emacs to take this change into account (or
+just run @kbd{M-x proof-shell-exit RET yes RET}
+and @kbd{M-x normal-mode RET} in the Coq buffer
+before restarting the Coq process).
+
 
 
 @node Using abbreviations