From 9d141fe86f68f2de7058d317874edc4c0885ebc6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 17 Feb 2015 18:21:44 +0100
Subject: Remove documentation of non-existing Show Implicits command.

---
 doc/refman/RefMan-pro.tex | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 08213abe9a..9055254bb5 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. 
-- 
cgit v1.2.3