diff options
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 7 |
1 files changed, 0 insertions, 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. |