diff options
| author | Théo Zimmermann | 2017-06-12 11:22:38 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-06-12 11:23:21 +0200 |
| commit | 6cd14bf253f681d0465f8dce1d84a54a4f104d9c (patch) | |
| tree | e7fb6bf346c09ff0cb705f299bdf9af6d941a808 /vernac | |
| parent | 76f97eac9e0b6eee76469b2a00a9c157caa3da8a (diff) | |
Remove non-working Show Tree and Show Node commands.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c0272f2108..e0eeaf563b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -61,11 +61,6 @@ let show_proof () = let pprf = Proof.partial_proof p in Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf) -let show_node () = - (* spiwack: I'm have little clue what this function used to do. I deactivated it, - could, possibly, be cleaned away. (Feb. 2010) *) - () - let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.") let show_top_evars () = @@ -83,9 +78,6 @@ let show_universes () = Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) -(* Spiwack: proof tree is currently not working *) -let show_prooftree () = () - (* Simulate the Intro(s) tactic *) let show_intro all = let open EConstr in @@ -1845,10 +1837,8 @@ let vernac_show = let open Feedback in function in msg_notice info | ShowProof -> show_proof () - | ShowNode -> show_node () | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () - | ShowTree -> show_prooftree () | ShowProofNames -> msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names())) | ShowIntros all -> show_intro all |