From 9914d778c0d62e8254ee6d0e68ead261edb7c71a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Jul 2000 10:10:25 +0000
Subject: index devenu list_index échoue maintenant avec Not_found et plus
 Failure

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

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 836b5e3efa..f97b32cd12 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -37,7 +37,7 @@ let make_elim_fun f largs =
 	let la' = list_map_i 
 		    (fun q aq ->
 		       try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) 
-		       with Failure _ -> aq) 1
+		       with Not_found -> aq) 1
                     (List.map (lift p) labs) 
 	in
 	list_fold_left_i 
-- 
cgit v1.2.3