diff options
| -rwxr-xr-x | doc/RefMan-uti.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex index 67f838127f..ccba33b48b 100755 --- a/doc/RefMan-uti.tex +++ b/doc/RefMan-uti.tex @@ -246,6 +246,10 @@ the \Coq\ language, and also a rudimentary indentation facility: \item M-{\sc Tab} decreases the indentation level. \end{itemize} +An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also +included in the distribution, in file \texttt{coq-inferior.el}. +Instructions to use it are contained in this file. + \subsection{Proof General}\index{Proof General} Proof General is a generic interface for proof assistants based on |