From 3a66d061535feb7093ab02a2adbad3843c41e7ad Mon Sep 17 00:00:00 2001
From: jnarboux
Date: Sat, 10 Jun 2006 12:04:14 +0000
Subject: ajout de la doc sur l'option -enable-geoproof de CoqIDE

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

diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index ea19f3de45..b771196688 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -11,9 +11,10 @@ them respectively. % CREDITS ? Proof general, lablgtk, ...
 \CoqIDE{} is run by typing the command \verb|coqide| on the command
 line. Without argument, the main screen is displayed with an ``unnamed
 buffer'', and with a file name as argument, another buffer displaying
-the contents of that file. Additionally, coqide accepts the same
-options as coqtop, given in Chapter~\ref{Addoc-coqc}, the ones having
-obviously no meaning for \CoqIDE{} being ignored.
+the contents of that file. Additionally, \verb|coqide| accepts the same
+options as \verb|coqtop|, given in Chapter~\ref{Addoc-coqc}, the ones having
+obviously no meaning for \CoqIDE{} being ignored. Additionally, \verb|coqide| accepts the option \verb|-enable-geoproof| to enable the support for \emph{GeoProof} \footnote{\emph{GeoProof} is dynamic geometry software which can be used in conjunction with \CoqIDE{} to interactively build a Coq statement corresponding to a geometric figure. More information about \emph{GeoProof} can be found here: \url{http://home.gna.org/geoproof/} }. 
+  
 
 \begin{figure}[t]
 \begin{center}
-- 
cgit v1.2.3