Merge PR#765: Remove obsolete Show commands

1 files changed, 0 insertions, 16 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 0760d716e..b66659dc8 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -427,22 +427,6 @@ This command displays the current goals.
   This tactics script may contain some holes (subgoals not yet proved).
   They are printed under the form \verb!<Your Tactic Text here>!.
 
-%% \item {\tt Show Tree.}\comindex{Show Tree}\\
-%% This command can be seen as a more structured way of
-%% displaying the state of the proof than that 
-%% provided by {\tt Show Script}. Instead of just giving
-%% the list of tactics that have been applied, it 
-%% shows the derivation tree constructed by then. 
-%% Each node of the tree contains the conclusion
-%% of the corresponding sub-derivation (i.e. a
-%% goal with its corresponding local context) and 
-%% the tactic that has generated all the 
-%% sub-derivations. The leaves of this tree are
-%% the goals which still remain to be proved.
-
-%\item {\tt Show Node}\comindex{Show Node}\\
-%        Not yet documented
-
 \item {\tt Show Proof.}\comindex{Show Proof}\\
 It displays the proof term generated by the 
 tactics that have been applied.