From cea76410557f9954c8e15861217bcc4559de9e25 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 11 Oct 2017 16:07:04 +0200
Subject: Remove GeoProof support.

Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
---
 doc/refman/RefMan-com.tex | 5 -----
 doc/refman/RefMan-ide.tex | 3 +--
 2 files changed, 1 insertion(+), 7 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 892c9931b6..8b1fc7c8f3 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -214,11 +214,6 @@ The following command-line options are recognized by the commands {\tt
 %
 %  Switch on the debug flag.
 
-\item[{\tt -with-geoproof} (yes|no)]\ %
-
-  Enable or not special functions for Geoproof within {\CoqIDE} (default
-  is yes).
-
 \item[{\tt -color} (on|off|auto)]\ %
 
   Enable or not the coloring of output of {\tt coqtop}. Default is auto,
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index 75f3d18ded..436099e74d 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -13,8 +13,7 @@ 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, \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/} }. 
-  
+obviously no meaning for \CoqIDE{} being ignored.
 
 \begin{figure}[t]
 \begin{center}
-- 
cgit v1.2.3