diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index be23d7729..c55e562a2 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -77,6 +77,8 @@ val is_done : proof -> bool (* Returns the list of partial proofs to initial goals. *) val partial_proof : proof -> Term.constr list +val compact : proof -> proof + (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. Raises [HasShelvedGoals] if some goals are left on the shelf. |