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

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

1 files changed, 25 insertions, 29 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d1005a8cd..8a4cdc3c7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -70,8 +70,8 @@ let def_of_const t =
     Const sp ->
       (try (match body_of_constant (Global.lookup_constant sp) with
              | Some c -> Lazyconstr.force c
-	     | _ -> assert false)
-       with _ ->
+	     | _ -> raise Not_found)
+       with Not_found ->
 	 anomaly (str "Cannot find definition of constant " ++
 		    (Id.print (Label.to_id (con_label sp))))
       )
@@ -237,15 +237,10 @@ let do_observe_tac s tac g =
     let v = tac g in 
     ignore(Stack.pop debug_queue);
     v
-  with e -> 
+  with reraise ->
     if not (Stack.is_empty debug_queue)
-    then
-      begin
-	let e : exn = Cerrors.process_vernac_interp_error e in
-	print_debug_queue true e
-      end
-    ; 
-    raise e
+    then print_debug_queue true (Cerrors.process_vernac_interp_error reraise);
+    raise reraise
 
 let observe_tac s tac g =
   if do_observe ()
@@ -392,7 +387,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 	    (fun g' -> 
 	      let ty_teq = pf_type_of g' (mkVar heq) in
 	      let teq_lhs,teq_rhs =
-		let _,args = try destApp ty_teq with _ -> assert false in
+		let _,args = try destApp ty_teq with DestKO -> assert false in
 		args.(1),args.(2)
 	      in
 	      let new_b' = Termops.replace_term teq_lhs teq_rhs new_b in 
@@ -495,23 +490,24 @@ and travel jinfo continuation_tac expr_info =
 
 let rec prove_lt hyple g = 
   begin
-    try 
-      let (_,args) = decompose_app (pf_concl g) in 
-      let x = try destVar (List.hd args) with _ -> assert false in 
-      let z = try destVar (List.hd (List.tl args)) with _ -> assert false in 
-      let h = 
-	List.find (fun id -> 
-	  let _,args' = decompose_app (pf_type_of g (mkVar id)) in  
-	  try x = destVar (List.hd args')
-	  with _ -> false
-	) hyple 
-      in 
-      let y = 
-	List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in 
+    try
+      let (varx,varz) = match decompose_app (pf_concl g) with
+        | _, x::z::_ when isVar x && isVar z -> x, z
+        | _ -> assert false
+      in
+      let h =
+	List.find (fun id ->
+          match decompose_app (pf_type_of g (mkVar id)) with
+            | _, t::_ -> eq_constr t varx
+            | _ -> false
+	) hyple
+      in
+      let y =
+	List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
       tclTHENLIST[
-	apply (mkApp(le_lt_trans (),[|mkVar x;y;mkVar z;mkVar h|]));
+	apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]));
 	observe_tac (str "prove_lt") (prove_lt hyple)
-      ]       
+      ]
     with Not_found -> 
       (
 	(
@@ -629,7 +625,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
       try 
 	check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b;
 	true
-      with _ -> false 
+      with e when Errors.noncritical e -> false
     in
     if forbid 
     then 
@@ -673,7 +669,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     try
       check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a;
       false
-    with _ ->
+    with e when Errors.noncritical e ->
       true
   in
   let a' = infos.info in
@@ -1207,7 +1203,7 @@ let is_rec_res id =
   let id_name = Id.to_string id in
   try
     String.sub id_name 0 (String.length rec_res_name) = rec_res_name
-  with _ -> false
+  with Invalid_argument _ -> false
  
 let clear_goals =
   let rec clear_goal t =