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

8 files changed, 62 insertions, 65 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index fdbd6cabd..ef4dca26d 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 a061cfaca..bb775d40a 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 2c44353f2..97512dd84 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 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 =
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 99eadd65d..2e8030ebf 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -331,9 +331,9 @@ let dual_raw_certificate (l:  (Poly.t * Mc.op1) list) =
     | Inr _ -> None
     | Inl cert ->  Some (rats_to_ints (Vect.to_list cert)) 
        (* should not use rats_to_ints *)
-  with x -> 
-   if debug 
-   then (Printf.printf "raw certificate %s" (Printexc.to_string x);   
+  with x when Errors.noncritical x ->
+   if debug
+   then (Printf.printf "raw certificate %s" (Printexc.to_string x);
          flush stdout) ;
    None
 
@@ -377,8 +377,9 @@ let linear_prover n_spec l  =
 
 
 let linear_prover n_spec l  =
- try linear_prover n_spec l with
-   x -> (print_string (Printexc.to_string x); None)
+ try linear_prover n_spec l
+ with x when Errors.noncritical x ->
+   (print_string (Printexc.to_string x); None)
 
 let linear_prover_with_cert spec l = 
   match linear_prover spec l with
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d2d6a7b63..eff1d4ba9 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -935,7 +935,8 @@ struct
                            let (expr,env) = parse_expr env args.(0) in
                            let power = (parse_exp expr args.(1)) in
                              (power  , env)
-			 with _ ->   (* if the exponent is a variable *)
+			 with e when Errors.noncritical e ->
+                           (* if the exponent is a variable *)
                            let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
                        end
                    | Ukn  s ->
@@ -1102,8 +1103,11 @@ struct
   
   let parse_formula parse_atom env tg term =
 
-    let parse_atom env tg t = try let (at,env) = parse_atom env t in
-                                    (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
+    let parse_atom env tg t =
+      try
+        let (at,env) = parse_atom env t in
+        (A(at,tg,t), env,Tag.next tg)
+      with e when Errors.noncritical e -> (X(t),env,tg) in
 
     let rec xparse_formula env tg term =
      match kind_of_term term with
@@ -1179,7 +1183,8 @@ let same_proof sg cl1 cl2 =
  let rec xsame_proof sg =
   match sg with
    | [] -> true
-   | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false)
+   | n::sg ->
+     (try List.nth cl1 n = List.nth cl2 n with Invalid_argument _ -> false)
       && (xsame_proof sg ) in
   xsame_proof sg
 
@@ -1243,7 +1248,7 @@ let btree_of_array typ a  =
 let btree_of_array typ a =
  try
   btree_of_array typ a
- with x ->
+ with x when Errors.noncritical x ->
   failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
 
 let dump_varmap typ env =
@@ -1312,7 +1317,7 @@ let rec parse_hyps parse_arith env tg hyps =
       try
        let (c,env,tg) = parse_formula parse_arith env  tg t in
 	((i,c)::lhyps, env,tg)
-      with _ -> 		(lhyps,env,tg)
+      with e when Errors.noncritical e -> (lhyps,env,tg)
        (*(if debug then Printf.printf "parse_arith : %s\n" x);*)
 
 
@@ -1456,7 +1461,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
           (pp_ml_list prover.pp_f) (List.map fst new_cl)   ;
           flush stdout
       end ; *)
-    let res = try prover.compact prf remap with x ->
+    let res = try prover.compact prf remap with x when Errors.noncritical x ->
       if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
       (* This should not happen -- this is the recovery plan... *)
       match prover.prover (List.map fst new_cl) with
@@ -2017,13 +2022,13 @@ let xlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ linear_Z ] gl
-  with z -> (*Printexc.print_backtrace stdout ;*) raise z
+  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 let xnlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ nlinear_Z ] gl
-  with z -> (*Printexc.print_backtrace stdout ;*) raise z
+  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 
 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 571c789c2..a1f08d568 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -727,8 +727,9 @@ struct
 	| Inl (s,_) ->
 	    try
 	      Some (bound_of_variable IMap.empty fresh s.sys)
-	    with
-		x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
+	    with x when Errors.noncritical x ->
+	      Printf.printf "optimise Exception : %s" (Printexc.to_string x);
+              None
 
 
   let find_point cstrs =
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 79db4a9c4..e8a72c055 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -225,7 +225,7 @@ let add_reified_atom t env =
     env.terms <- env.terms @ [t]; i
 
 let get_reified_atom env =
-  try List.nth env.terms with _ -> failwith "get_reified_atom"
+  try List.nth env.terms with Invalid_argument _ -> failwith "get_reified_atom"
 
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
@@ -235,7 +235,8 @@ let add_prop env t =
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
 (* accès a une proposition *)
-let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
+let get_prop v env =
+  try List.nth v env with Invalid_argument _ -> failwith "get_prop"
 
 (* \subsection{Gestion du nommage des équations} *)
 (* Ajout d'une equation dans l'environnement de reification *)