From fed5cbc5b006447bb3d877b3eeb35f7c76e96661 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:34:06 +0000
Subject: Uses Proofview.tclEXTEND more sparingly.

It is used where failures can be caughts (tclORELSE, tclTRY, …) rather than
at each tclTHEN. Hopefully avoiding making things a bit less slow.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16968 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proofview.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3