From 3e5ba8bb1188e9c0f59c04bd0e8fa7c9ff5bc52b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 4 Nov 2017 15:59:31 +0100
Subject: Finish removing Show Goal uid

Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
---
 printing/printer.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 658ea6060..f55206f0d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -201,7 +201,6 @@ val pr_assumptionset :
   env -> Term.types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : Id.t -> Pp.t
-val pr_goal_by_uid : string -> Pp.t
 
 type printer_pr = {
  pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
-- 
cgit v1.2.3