diff options
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 |