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 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

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