From 95e97b68744eeb8bf20811c3938d78912eb3e918 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 24 Jul 2014 17:42:10 +0200
Subject: Goal: API to get the solution of a goal

---
 proofs/goal.ml  | 5 +++++
 proofs/goal.mli | 1 +
 2 files changed, 6 insertions(+)

diff --git a/proofs/goal.ml b/proofs/goal.ml
index c31375f9e0..ae6ec558b9 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -83,6 +83,11 @@ let rec advance sigma g =
       else
         None
 
+let solution sigma g =
+  let evi = Evd.find sigma g.content in
+  match evi.Evd.evar_body with
+  | Evd.Evar_empty -> None
+  | Evd.Evar_defined v -> Some v
 
 (* Equality function on goals *)
 let equal evars1 gl1 evars2 gl2 =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 87793878cf..696c91dc58 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -30,6 +30,7 @@ val pr_goal : goal -> Pp.std_ppcmds
     into [g']). It returns [None] if [g] has been (partially) solved. *)
 val advance : Evd.evar_map -> goal -> goal option
 
+val solution : Evd.evar_map -> goal -> Term.constr option
 
 (* Equality function on goals. Return [true] if all of its hypotheses
    and conclusion are equal. *)
-- 
cgit v1.2.3