diff options
| -rw-r--r-- | intf/vernacexpr.ml | 1 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
4 files changed, 0 insertions, 8 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index ab440c6b71..c928e0bbbf 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 e2d0aed73a..8c270d8024 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 781af47892..2633cdd6b5 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 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 () |