diff options
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/goal.mli | 1 |
2 files changed, 6 insertions, 0 deletions
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. *) |