diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ce2decc3e4..388778ff7d 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -313,7 +313,7 @@ let rec tclDISPATCHGEN null join tacs env = Inner.get >>= fun step' -> Inner.set {step' with comb=step.comb@step'.comb} >> Inner.return (join x y) - | _ , _ -> raise SizeMismatch + | _ , _ -> tclZERO SizeMismatch env let unitK () () = () let tclDISPATCH = tclDISPATCHGEN () unitK |