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