From 13b1bba79256fa406a4c7a24ae7b395c33e69212 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 15 Apr 2002 12:43:33 +0000
Subject: mention de coq-inferior.el

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8278 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-uti.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc')

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
-- 
cgit v1.2.3