diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index fd5e905a3b..40e8ff7eef 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -130,13 +130,10 @@ val compact : t -> t (* 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. - Raises [HasGivenUpGoals] if some goals have been given up. - Raises [HasUnresolvedEvar] if some evars have been left undefined. *) + Raises [HasGivenUpGoals] if some goals have been given up. *) type open_error_reason = | UnfinishedProof - | HasShelvedGoals | HasGivenUpGoals - | HasUnresolvedEvar exception OpenProof of Names.Id.t option * open_error_reason |