diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-08 12:52:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-08 12:52:05 +0200 |
| commit | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (patch) | |
| tree | 3dc155ac0aab0bd845debefc8805cdd1106cd52f /proofs/proofview.mli | |
| parent | 0aec33ac7ede9098b5cef9ce467bfad5aca8b379 (diff) | |
Display number of available goals in "incorrect number of goals" error message.
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index ae18934e7..681690810 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -216,8 +216,9 @@ val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic the corresponding goal. When the length of the tactic list is not the number of goal, - raises [SizeMismatch] *) -exception SizeMismatch + raises [SizeMismatch (g,t)] where [g] is the number of available + goals, and [t] the number of tactics passed. *) +exception SizeMismatch of int*int val tclDISPATCH : unit tactic list -> unit tactic val tclDISPATCHL : 'a tactic list -> 'a list tactic |