diff options
| author | glondu | 2010-10-06 18:57:04 +0000 |
|---|---|---|
| committer | glondu | 2010-10-06 18:57:04 +0000 |
| commit | 2fe6aa3b4d422ec092844e84c4d15f5c1414b442 (patch) | |
| tree | 55b5e6255d514cc05b72b0041fd567dd0d11132d /toplevel | |
| 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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
2 files changed, 0 insertions, 14 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7d342737c7..7797db4730 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 f3aa076ada..36c2b26c01 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 |