diff options
| author | Jim Fehrle | 2018-08-08 18:45:47 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-09-17 10:33:27 -0700 |
| commit | a828bcedb8ad60c5b1f4cf71f92f24f2c1197ecb (patch) | |
| tree | 372fd5a8c6f880db4f246ea5b6f498a7393bc737 /proofs/proof.mli | |
| parent | f1482433ff225831d9937753f946cff2577b9309 (diff) | |
Ensure_prev_proof returns a proof that has underlying differences from
the specified version (i.e., skip over versions with proofview-only differences).
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 |