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


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

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index c928e0bbbf..b3b3327272 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
-- 
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 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index b3b3327272..cabd06735f 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
-- 
cgit v1.2.3