diff options
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 8cf543557b..aaabea3454 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -89,11 +89,15 @@ val compact : t -> t 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. *) -exception UnfinishedProof -exception HasShelvedGoals -exception HasGivenUpGoals -exception HasUnresolvedEvar -val return : t -> Evd.evar_map +type open_error_reason = + | UnfinishedProof + | HasShelvedGoals + | HasGivenUpGoals + | HasUnresolvedEvar + +exception OpenProof of Names.Id.t option * open_error_reason + +val return : ?pid:Names.Id.t -> t -> Evd.evar_map (*** Focusing actions ***) |