diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 6 |
1 files changed, 4 insertions, 2 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 *) |