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
---
 parsing/astterm.ml  | 4 ++--
 pretyping/tacred.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index e0e705ee9d..d41e692339 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -290,7 +290,7 @@ let dbize k sigma env allow_soapp lvar =
 	let n =
 	  try 
 	    (list_index (ident_of_nvar locid iddef) lf) -1
-          with Failure _ ->
+          with Not_found ->
 	    error_fixname_unbound "dbize (FIX)" false locid iddef in
 	let ext_env =
 	  List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
@@ -303,7 +303,7 @@ let dbize k sigma env allow_soapp lvar =
 	let n =
           try 
 	    (list_index (ident_of_nvar locid iddef) lf) -1
-          with Failure _ ->
+          with Not_found ->
 	    error_fixname_unbound "dbize (COFIX)" true locid iddef in
 	let ext_env =
 	  List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
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