diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 18:57:04 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-06 18:57:04 +0000 |
commit | 2fe6aa3b4d422ec092844e84c4d15f5c1414b442 (patch) | |
tree | 55b5e6255d514cc05b72b0041fd567dd0d11132d | |
parent | b36e75cca2ea910dead09864c4f10ba79b894a35 (diff) |
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
-rw-r--r-- | dev/v8-syntax/syntax-v8.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-oth.tex | 3 | ||||
-rw-r--r-- | parsing/g_proofs.ml4 | 4 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 12 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 2 |
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 |