From 3e5ba8bb1188e9c0f59c04bd0e8fa7c9ff5bc52b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 4 Nov 2017 15:59:31 +0100
Subject: Finish removing Show Goal uid

Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
---
 vernac/vernacentries.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e08cb83871..425cf8fb0c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1853,7 +1853,6 @@ let vernac_show = let open Feedback in function
       | OpenSubgoals -> pr_open_subgoals ()
       | NthGoal n -> pr_nth_open_subgoal n
       | GoalId id -> pr_goal_by_id id
-      | GoalUid id -> pr_goal_by_uid id
     in
     msg_notice info
   | ShowProof -> show_proof ()
-- 
cgit v1.2.3