diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-15 12:43:33 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-15 12:43:33 +0000 |
| commit | 13b1bba79256fa406a4c7a24ae7b395c33e69212 (patch) | |
| tree | d4aa17895efd61f24dc8ccc2c4176100b2dea25a /doc/RefMan-uti.tex | |
| 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
Diffstat (limited to 'doc/RefMan-uti.tex')
| -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 67f838127..ccba33b48 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 |