From faa064c746e20a12b3c8f792f69537b18e387be6 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:02:13 +0200
Subject: Remove Show Goal "uid" command.

Introduced for Proof-General but unused at the current time,
undocumented and can raise anomalies.
---
 parsing/g_proofs.ml4 | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index a3f9793bbd..e2d0aed73a 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -64,9 +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 "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal")))
-      | IDENT "Show"; IDENT "Goal"; n = string ->
-          VernacShow (ShowGoal (GoalUid n))
       | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
 	  VernacShow (ShowGoalImplicitly n)
       | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
-- 
cgit v1.2.3