diff options
| author | aspiwack | 2013-11-04 18:08:43 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-04 18:08:43 +0000 |
| commit | e3d3d73dfca0576cb25ce555cc445c657baecb19 (patch) | |
| tree | 0499dd493ba52659e0fd201f30a4738d355bc7c2 /proofs/proofview.mli | |
| parent | 0e24703029ecdbc87146a3bcf50faecf18a8c583 (diff) | |
Fix the tactical ; [ … ] : the "incorrect number of goal" error was not caught by ltac tacticals.
The errors were not translated into ltac errors (and at some occurence errors were raised in OCaml rather than inside the tactic monad).
Spotted in ProjectiveGeometry and Goedel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proofview.mli')
| -rw-r--r-- | proofs/proofview.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2945fb7141..8bd7b8a283 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -179,7 +179,11 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic goal (starting with the first goal). In the case of [tclDISPATCHL], the tactic returns a list of the same size as the argument list (of tactics), each element being the result of the tactic executed in - the corresponding goal. *) + the corresponding goal. + + When the length of the tactic list is not the number of goal, + raises [SizeMismatch] *) +exception SizeMismatch val tclDISPATCH : unit tactic list -> unit tactic val tclDISPATCHL : 'a tactic list -> 'a list tactic |