diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-10-11 16:07:04 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-11 16:07:04 +0200 |
commit | cea76410557f9954c8e15861217bcc4559de9e25 (patch) | |
tree | 853557ca2abcce31cc5dbcc77da58df7675f6e48 /doc | |
parent | 354ee7d67efda8624cb46e942f2a41211cadd030 (diff) |
Remove GeoProof support.
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-com.tex | 5 | ||||
-rw-r--r-- | doc/refman/RefMan-ide.tex | 3 |
2 files changed, 1 insertions, 7 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 892c9931b..8b1fc7c8f 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 75f3d18de..436099e74 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} |