diff options
| author | filliatr | 2002-04-15 12:43:33 +0000 |
|---|---|---|
| committer | filliatr | 2002-04-15 12:43:33 +0000 |
| commit | 13b1bba79256fa406a4c7a24ae7b395c33e69212 (patch) | |
| tree | d4aa17895efd61f24dc8ccc2c4176100b2dea25a | |
| parent | 3e54a24034550eaae6ac367dcda68e9c01b173d1 (diff) | |
mention de coq-inferior.el
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8278 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |