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

---
 proofs/goal.ml  | 3 ++-
 proofs/goal.mli | 2 ++
 2 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index dc55c8179a..55de872612 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -31,9 +31,10 @@ type goal = {
 (* spiwack: I don't deal with the tags, yet. It is a worthy discussion
    whether we do want some tags displayed besides the goal or not. *)
 
-
 let pr_goal {content = e} = str "GOAL:" ++ Pp.int (Evar.repr e)
 
+let goal_ident sigma {content = e} = Evd.evar_ident e sigma
+
 (* access primitive *)
 (* invariant : [e] must exist in [em] *)
 let content evars { content = e } = Evd.find evars e
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 4d3361b0e3..4b85ec20b1 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