From 4e643d134f02cfa9a73754c3cf48048541324834 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2015 15:49:09 +0100
Subject: Adding syntax "Show id" to show goal named id (shelved or not).

---
 printing/printer.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 0a44e4f103..5c60b89366 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -176,7 +176,8 @@ module ContextObjectMap : CMap.ExtS
 val pr_assumptionset :
   env -> Term.types ContextObjectMap.t -> std_ppcmds
 
-val pr_goal_by_id : string -> std_ppcmds
+val pr_goal_by_id : Id.t -> std_ppcmds
+val pr_goal_by_uid : string -> std_ppcmds
 
 type printer_pr = {
  pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
-- 
cgit v1.2.3