From c332c8fe84f7a2f1abbde26a95a369934ed82487 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 21 Nov 2000 16:51:32 +0000
Subject: PatternMatchingFailure n'etait pas rattrapee

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0ae6ecb7f4..9228013be5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -774,7 +774,7 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
 		 []
 	       else
 		 matches (pattern_of_constr headpat) ty 
-             with e when catchable_exception e -> failwith "caught")
+             with PatternMatchingFailure -> failwith "caught")
 	  [dFLTty; nf_ty]
       in
       (bindings,dFLT)
-- 
cgit v1.2.3