diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 20088fd72a..87ec076faf 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -187,10 +187,6 @@ Section~\ref{LongNames}). it in {\em file}{\tt .beautified} in order to get old-fashion syntax/definitions/notations. -\item[{\tt -quality}] - - Improve the legibility of the proof terms produced by some tactics. - \item[{\tt -emacs}, {\tt -ide-slave}]\ Start a special main loop to communicate with ide. |