diff options
| author | Enrico Tassi | 2014-07-24 17:42:10 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-08-05 18:24:50 +0200 |
| commit | 95e97b68744eeb8bf20811c3938d78912eb3e918 (patch) | |
| tree | f6cf7cfcbdb94ea6f014354df4d75c3f4fe10405 /proofs | |
| parent | ed4d62c2a4ef8cc6796dfa03662900be67339ff9 (diff) | |
Goal: API to get the solution of a goal
Diffstat (limited to 'proofs')
| -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. *) |