diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview.mli | 6 |
2 files changed, 9 insertions, 3 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 7eb32f34a2..bbeed4ad10 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -460,8 +460,10 @@ let tclEXTEND tacs1 rtac tacs2 = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in Proof.get >>= fun step -> - let tacs = extend_to_list tacs1 rtac tacs2 step.comb in - tclDISPATCH tacs + try + let tacs = extend_to_list tacs1 rtac tacs2 step.comb in + tclDISPATCH tacs + with SizeMismatch -> tclZERO SizeMismatch let tclINDEPENDENT tac = (* spiwack: convenience notations, waiting for ocaml 3.12 *) 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 |