Remove Explain* vernacs

Basically untouched since 1999. Same fate as VernacGo (r13506).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13510 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 0 insertions, 25 deletions

diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 46ba24da7..4fb47bea7 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1179,8 +1179,6 @@ $$
 \nlsep \TERM{Show}~\TERM{Intros}
 %% Correctness: obsolete ?
 %%\nlsep \TERM{Show}~\TERM{Programs}
-\nlsep \TERM{Explain}~\TERM{Proof}~\OPT{\TERM{Tree}}~\STAR{\NT{num}}
-%% Go not documented
 \nlsep \TERM{Hint}~\OPT{\TERM{Local}}~\NT{hint}~\OPT{\NT{inbases}}
 %% PrintConstr not documented
 \end{rules}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index c1dc35dcb..2a0b8051c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -969,9 +969,6 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\comindex{Test Printing Depth}}
 This command displays the current nesting depth used for display.
 
-%\subsection{\tt Explain ...}
-%Not yet documented.
-
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index b5bac26c3..e23ef9143 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -80,10 +80,6 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
       | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
       | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis
-      | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
-	  VernacShow (ExplainProof l)
-      | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer ->
-	  VernacShow (ExplainTree l)
       | IDENT "Guarded" -> VernacCheckGuard
 (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 24c9d9d8a..0a65578f1 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -464,8 +464,6 @@ let rec pr_vernac = function
 	| ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro")
 	| ShowMatch id -> str"Show Match " ++ pr_lident id
 	| ShowThesis -> str "Show Thesis"
-	| ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l
-	| ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l
       in pr_showable s
   | VernacCheckGuard -> str"Guarded"
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7d342737c..7797db473 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1237,16 +1237,6 @@ let vernac_end_subproof () =
   let p = Proof_global.give_me_the_proof () in
   Proof.unfocus subproof_kind p ; print_subgoals ()
 
-let explain_proof occ =
-  (* spiwack: don't know what it's supposed to do. Undocumented. 
-     Deactivated and candidate for removal. (Feb. 2010) *)
-  ()
-
-let explain_tree occ =
-  (* spiwack: don't know what it's supposed to do. Undocumented.
-     Deactivated and candidate for removeal. (Feb. 2010) *)
-  ()
-
 let vernac_show = function
   | ShowGoal nopt ->
       if !pcoq <> None then (Option.get !pcoq).show_goal nopt
@@ -1267,8 +1257,6 @@ let vernac_show = function
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
   | ShowThesis -> show_thesis ()
-  | ExplainProof occ -> explain_proof occ
-  | ExplainTree occ -> explain_tree occ
 
 
 let vernac_check_guard () =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index f3aa076ad..36c2b26c0 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -93,8 +93,6 @@ type showable =
   | ShowIntros of bool
   | ShowMatch of lident
   | ShowThesis
-  | ExplainProof of int list
-  | ExplainTree of int list
 
 type comment =
   | CommentConstr of constr_expr