From faa064c746e20a12b3c8f792f69537b18e387be6 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 12 Jun 2017 11:02:13 +0200 Subject: Remove Show Goal "uid" command. Introduced for Proof-General but unused at the current time, undocumented and can raise anomalies. --- parsing/g_proofs.ml4 | 3 --- 1 file changed, 3 deletions(-) (limited to 'parsing/g_proofs.ml4') diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index a3f9793bb..e2d0aed73 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -64,9 +64,6 @@ GEXTEND Gram | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) - | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal"))) - | IDENT "Show"; IDENT "Goal"; n = string -> - VernacShow (ShowGoal (GoalUid n)) | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode -- cgit v1.2.3 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. --- intf/vernacexpr.ml | 1 - parsing/g_proofs.ml4 | 2 -- printing/ppvernac.ml | 1 - vernac/vernacentries.ml | 4 ---- 4 files changed, 8 deletions(-) (limited to 'parsing/g_proofs.ml4') diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index ab440c6b7..c928e0bbb 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -96,7 +96,6 @@ type locatable = type showable = | ShowGoal of goal_reference - | ShowGoalImplicitly of int option | ShowProof | ShowNode | ShowScript diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e2d0aed73..8c270d802 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -64,8 +64,6 @@ GEXTEND Gram | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) - | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> - VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 781af4789..2633cdd6b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -561,7 +561,6 @@ open Decl_kinds | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n - | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n | ShowProof -> keyword "Show Proof" | ShowNode -> keyword "Show Node" | ShowScript -> keyword "Show Script" diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ef16df5b7..c0272f210 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. --- intf/vernacexpr.ml | 2 -- parsing/g_proofs.ml4 | 2 -- printing/ppvernac.ml | 2 -- vernac/vernacentries.ml | 10 ---------- 4 files changed, 16 deletions(-) (limited to 'parsing/g_proofs.ml4') diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index c928e0bbb..b3b332727 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -97,11 +97,9 @@ type locatable = type showable = | ShowGoal of goal_reference | ShowProof - | ShowNode | ShowScript | ShowExistentials | ShowUniverses - | ShowTree | ShowProofNames | ShowIntros of bool | ShowMatch of reference diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 8c270d802..b5eb2a181 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -64,11 +64,9 @@ GEXTEND Gram | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) - | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses - | IDENT "Show"; IDENT "Tree" -> VernacShow ShowTree | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2633cdd6b..81f41cba1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -562,11 +562,9 @@ open Decl_kinds let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowProof -> keyword "Show Proof" - | ShowNode -> keyword "Show Node" | ShowScript -> keyword "Show Script" | ShowExistentials -> keyword "Show Existentials" | ShowUniverses -> keyword "Show Universes" - | ShowTree -> keyword "Show Tree" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") | ShowMatch id -> keyword "Show Match " ++ pr_reference id diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c0272f210..e0eeaf563 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. --- intf/vernacexpr.ml | 1 - parsing/g_proofs.ml4 | 1 - printing/ppvernac.ml | 1 - vernac/vernacentries.ml | 4 ---- 4 files changed, 7 deletions(-) (limited to 'parsing/g_proofs.ml4') diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index b3b332727..cabd06735 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -103,7 +103,6 @@ type showable = | ShowProofNames | ShowIntros of bool | ShowMatch of reference - | ShowThesis type comment = | CommentConstr of constr_expr diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index b5eb2a181..e96a68bc6 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -72,7 +72,6 @@ GEXTEND Gram | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) - | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 81f41cba1..9d28bc4f8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -568,7 +568,6 @@ open Decl_kinds | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") | ShowMatch id -> keyword "Show Match " ++ pr_reference id - | ShowThesis -> keyword "Show Thesis" in return (pr_showable s) | VernacCheckGuard -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e0eeaf563..6830a5da1 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