From c04a214b50698cb8747e4e08fcc5cd52021068ad Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Jun 2002 14:24:09 +0000
Subject: Passage de PatternMatchingFailure vers UserError pour capture par
 tclFIRST

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

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 720cb6f5f1..d73677617b 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -244,7 +244,9 @@ let forward_tac_interp =
 let set_extern_interp f = forward_tac_interp := f
 
 let applyDestructor cls discard dd gls =
-  let mvb = match_dpat dd.d_pat cls gls in
+  let mvb =
+    try match_dpat dd.d_pat cls gls
+    with PatternMatchingFailure -> error "No match" in
   let tac = match cls with
     | Some id -> 
 	let arg = Reference (RIdent (dummy_loc,id)) in
-- 
cgit v1.2.3