diff options
| -rw-r--r-- | proofs/proofview.ml | 6 | ||||
| -rw-r--r-- | proofs/proofview.mli | 6 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 23 |
3 files changed, 24 insertions, 11 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 diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 299a1e1768..bcb6041eff 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -415,24 +415,31 @@ module New = struct let tclTHENS3PARTS t1 l1 repeat l2 = tclINDEPENDENT begin - t1 <*> tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) + t1 <*> + Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) + begin tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) end + begin function + | SizeMismatch -> tclFAIL 0 (str"Incorrect number of goals") + | reraise -> tclZERO reraise + end end let tclTHENSFIRSTn t1 l repeat = tclTHENS3PARTS t1 l repeat [||] let tclTHENFIRSTn t1 l = tclTHENSFIRSTn t1 l (tclUNIT()) let tclTHENFIRST t1 t2 = - tclEXTEND [] begin - t1 <*> tclFOCUS 1 1 t2 - end [] + tclTHENFIRSTn t1 [|t2|] let tclTHENLASTn t1 l = - tclINDEPENDENT begin - t1 <*> tclEXTEND [] (tclUNIT()) (Array.to_list l) - end + tclTHENS3PARTS t1 [||] (tclUNIT()) l let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] let tclTHENS t l = tclINDEPENDENT begin - t <*> tclDISPATCH l + t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) + begin tclDISPATCH l end + begin function + | SizeMismatch -> tclFAIL 0 (str"Incorrect number of goals") + | reraise -> tclZERO reraise + end end let tclTHENLIST l = List.fold_left tclTHEN (tclUNIT()) l |