diff options
| author | Emilio Jesus Gallego Arias | 2018-09-23 14:25:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-23 14:25:37 +0200 |
| commit | 8c15896b3d3cbfc11f5c493282be3dc1c5c27315 (patch) | |
| tree | 343a65c42914ec32485bc2ea5572476fc36d6c43 /proofs/proof.mli | |
| parent | 033f3aef06f627b1db762577aac11545e5b7a07f (diff) | |
| parent | 2dc65d41b0c3b3481958e1e224fd5ef05f57f243 (diff) | |
Merge PR #8247: Show diffs on multiple changed goals; match old and new goal info
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 33addf13d7..511dcc2e00 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -210,3 +210,6 @@ module V82 : sig (* Implements the Existential command *) val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end + +(* returns the set of all goals in the proof *) +val all_goals : t -> Goal.Set.t |