From d542746c848d4795d4af97874a30fa5e98c8a6b2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 21 Aug 2014 12:23:06 +0200
Subject: Use evar name to print goal.

---
 proofs/goal.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs/goal.mli')

diff --git a/proofs/goal.mli b/proofs/goal.mli
index 4d3361b0e..4b85ec20b 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -25,6 +25,8 @@ val get_by_uid : string -> goal
 (* Debugging help *)
 val pr_goal : goal -> Pp.std_ppcmds
 
+val goal_ident : Evd.evar_map -> goal -> Names.Id.t
+
 (* [advance sigma g] returns [Some g'] if [g'] is undefined and 
     is the current avatar of [g] (for instance [g] was changed by [clear]
     into [g']). It returns [None] if [g] has been (partially) solved. *)
-- 
cgit v1.2.3