From 2253d2eb4f892f932332358be8537fdb5552ef87 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:08:12 +0200
Subject: Remove Show Implicit Arguments command.

The command has been broken for 15 years. It is basically dead code.
Its former behavior can be mimicked with Set Printing Implicit. Show.
---
 vernac/vernacentries.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..c0272f2108 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1844,10 +1844,6 @@ let vernac_show = let open Feedback in function
       | GoalUid id -> pr_goal_by_uid id
     in
     msg_notice info
-  | ShowGoalImplicitly None ->
-      Constrextern.with_implicits msg_notice (pr_open_subgoals ())
-  | ShowGoalImplicitly (Some n) ->
-      Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n)
   | ShowProof -> show_proof ()
   | ShowNode -> show_node ()
   | ShowExistentials -> show_top_evars ()
-- 
cgit v1.2.3


From 6cd14bf253f681d0465f8dce1d84a54a4f104d9c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:22:38 +0200
Subject: Remove non-working Show Tree and Show Node commands.

---
 vernac/vernacentries.ml | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3


From 3813ba5229cf42597cd30a08e842e0832e5253cb Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:25:26 +0200
Subject: Remove Show Thesis command which was never implemented.

---
 vernac/vernacentries.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e0eeaf563b..6830a5da1a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -61,8 +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_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.")
-
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
   let pfts = get_pftreestate () in
@@ -1843,8 +1841,6 @@ let vernac_show = let open Feedback in function
       msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
-  | ShowThesis -> show_thesis ()
-
 
 let vernac_check_guard () =
   let pts = get_pftreestate () in
-- 
cgit v1.2.3