Remove documentation of non-existing Show Implicits command.

1 files changed, 0 insertions, 7 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 08213abe9..9055254bb 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -400,13 +400,6 @@ This command displays the current goals.
 \item \errindex{No focused proof}
 \end{ErrMsgs}
 
-\item {\tt Show Implicits.}\comindex{Show Implicits}\\
-  Displays the current goals, printing the implicit arguments of
-  constants.
-
-\item {\tt Show Implicits {\num}.}\\
-  Same as above, only displaying the {\num}-th subgoal.
-
 \item {\tt Show Script.}\comindex{Show Script}\\
   Displays the whole list of tactics applied from the beginning
   of the current proof.