Restrict (try...with...) to avoid catching critical exn (part 7)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 9 insertions, 11 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index be3817d5e5..89e6bf8225 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -274,7 +274,7 @@ let is_nondep_branch c n =
   try
     let sign,ccl = decompose_lam_n_assum n c in
     noccur_between 1 (rel_context_length sign) ccl
-  with _ -> (* Not eta-expanded or not reduced *)
+  with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
 
 let extract_nondep_branches test c b n =
@@ -391,10 +391,8 @@ let rec detype (isgoal:bool) avoid env t =
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
 	GEvar (dl, n, None)
     | Var id ->
-	(try
-	  let _ = Global.lookup_named id in GRef (dl, VarRef id)
-	 with _ ->
-	  GVar (dl, id))
+	(try let _ = Global.lookup_named id in GRef (dl, VarRef id)
+	 with Not_found -> GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
         detype isgoal avoid env c1
@@ -506,7 +504,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
     let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
     List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
       mat
-  with _ ->
+  with e when Errors.noncritical e ->
     Array.to_list
       (Array.map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 72de7f4719..1396f91d4f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1049,8 +1049,8 @@ let meta_reducible_instance evd b =
   let rec irec u =
     let u = whd_betaiota Evd.empty u in
     match kind_of_term u with
-    | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
-	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
+    | Case (ci,p,c,bl) when isMeta (strip_outer_cast c) ->
+	let m = destMeta (strip_outer_cast c) in
 	(match
 	  try
 	    let g, s = List.assoc m metas in
@@ -1060,8 +1060,8 @@ let meta_reducible_instance evd b =
 	  with
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
-    | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
-	let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
+    | App (f,l) when isMeta (strip_outer_cast f) ->
+	let m = destMeta (strip_outer_cast f) in
 	(match
 	  try
 	    let g, s = List.assoc m metas in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 1ccc103755..fb8a05a97f 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -44,7 +44,7 @@ let invert_tag cst tag reloc_tbl =
 let find_rectype_a env c =
   let (t, l) =
     let t = whd_betadeltaiota env c in
-    try destApp t with _ -> (t,[||]) in
+    try destApp t with DestKO -> (t,[||]) in
   match kind_of_term t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found