diff options
| author | Théo Zimmermann | 2017-06-12 11:08:12 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-06-12 11:08:12 +0200 |
| commit | 2253d2eb4f892f932332358be8537fdb5552ef87 (patch) | |
| tree | 78825c9f5c9db43fc1e1b03ca26ba73cbdd98cfd /vernac | |
| parent | faa064c746e20a12b3c8f792f69537b18e387be6 (diff) | |
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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 0 insertions, 4 deletions
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 () |