diff options
| author | Maxime Dénès | 2019-01-17 10:53:19 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-21 10:26:04 +0100 |
| commit | 945f49236e0db8179548110a056f9787ecffd746 (patch) | |
| tree | c3c350f7f6279cab7bd572069ce3846be77145fe /proofs/proof.mli | |
| parent | 10a9c492a486fcb884ffeadd1d05ecb0fae90d0f (diff) | |
At Qed, if shelved goals remain, emit a warning instead of an error
This error was more or less a debug tool (checking that no tactic breaks
the invariant). But some users may want to support other models, see
https://github.com/Mtac2/Mtac2/pull/139 for an example discussion.
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 |