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

4 files changed, 36 insertions, 47 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index fdbd6cabd2..ef4dca26de 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -73,16 +73,9 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
-    begin
-      if not (Stack.is_empty debug_queue)
-      then
-	begin
-	  let reraise : exn = Cerrors.process_vernac_interp_error reraise in
-	  print_debug_queue true reraise
-	end
-      ;
-      raise reraise
-    end
+    if not (Stack.is_empty debug_queue)
+    then print_debug_queue true (Cerrors.process_vernac_interp_error reraise);
+    raise reraise
 
 let observe_tac_stream s tac g =
   if do_observe ()
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index a061cfaca7..bb775d40a4 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -63,11 +63,11 @@ let do_observe_tac s tac g =
   let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
   try
     let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
-  with e ->
-    let e' = Cerrors.process_vernac_interp_error e in
+  with reraise ->
+    let e = Cerrors.process_vernac_interp_error reraise in
     msgnl (str "observation "++ s++str " raised exception " ++
-	     Errors.print e' ++ str " on goal " ++ goal );
-    raise e;;
+	     Errors.print e ++ str " on goal " ++ goal );
+    raise reraise;;
 
 
 let observe_tac_strm s tac g =
@@ -824,7 +824,7 @@ let rec reflexivity_with_destruct_cases g =
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
 	| _ -> reflexivity
-    with _ -> reflexivity
+    with e when Errors.noncritical e -> reflexivity
   in
   let eq_ind =     Coqlib.build_coq_eq () in
   let discr_inject =
@@ -1118,11 +1118,11 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs;
-  with e ->
+  with reraise ->
     (* In case of problem, we reset all the lemmas *)
     Pfedit.delete_all_proofs ();
     States.unfreeze previous_state;
-    raise e
+    raise reraise
 
 
 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 2c44353f26..97512dd846 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -71,7 +71,7 @@ let ident_global_exist id =
     let ans = CRef (Libnames.Ident (Loc.ghost,id)) in
     let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
     true
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 (** [next_ident_fresh id] returns a fresh identifier (ie not linked in
     global env) with base [id]. *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d1005a8cd3..8a4cdc3c72 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 =