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

15 files changed, 61 insertions, 88 deletions

diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index b940dee3a..626629063 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -164,20 +164,19 @@ qui donne 0 < c si s=true
        ou 0 <= c sinon
 cette inéquation étant absurde.
 *)
+
+exception Contradiction of (rational * bool * rational list) list
+
 let unsolvable lie =
    let lr = deduce lie in
-   let res = ref [] in
-   (try (List.iter (fun e ->
-         match e with
-           {coef=[c];hist=lc;strict=s} ->
-		  if (rinf c r0 && (not s)) || (rinfeq c r0 && s)
-                  then (res := [c,s,lc];
-			raise (Failure "contradiction found"))
-          |_->assert false)
-			     lr)
-   with _ -> ());
-   !res
-;;
+   let check = function
+     | {coef=[c];hist=lc;strict=s} ->
+       if (rinf c r0 && (not s)) || (rinfeq c r0 && s)
+       then raise (Contradiction [c,s,lc])
+     |_->assert false
+   in
+   try List.iter check lr; []
+   with Contradiction l -> l
 
 (* Exemples:
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index fbb00285c..0ec82425d 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -40,7 +40,7 @@ type flin = {fhom: rational Constrhash.t;
 
 let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
 
-let flin_coef f x = try (Constrhash.find f.fhom x) with _-> r0;;
+let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;;
 
 let flin_add f x c =
     let cx = flin_coef f x in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a5e7d6c4d..f8ea1d528 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1224,7 +1224,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
 	let pte,pte_args = (decompose_app pte_app) in
 	try
-	  let pte = try destVar pte with _ -> anomaly (Pp.str "Property is not a variable")  in
+	  let pte =
+            try destVar pte
+            with DestKO -> anomaly (Pp.str "Property is not a variable")
+          in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 131b4c0e2..d58a6f038 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -85,10 +85,7 @@ let functional_induction with_clean c princl pat =
     let princ' = Some (princ,bindings) in
     let princ_vars =
       List.fold_right
-	(fun a acc ->
-	  try Id.Set.add (destVar a) acc
-	  with _ -> acc
-	)
+	(fun a acc -> try Id.Set.add (destVar a) acc with DestKO -> acc)
 	args
 	Id.Set.empty
     in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 67f6fdd54..d6a017d08 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -49,11 +49,8 @@ let locate_constant ref =
 
 
 let locate_with_msg msg f x =
-  try
-    f x
-  with
-    | Not_found -> raise (Errors.UserError("", msg))
-    | e -> raise e
+  try f x
+  with Not_found -> raise (Errors.UserError("", msg))
 
 
 let filter_map filter f =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bea019259..d1005a8cd 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1491,7 +1491,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
 	  false
-      with e ->
+      with e when Errors.noncritical e ->
 	begin
 	  if do_observe ()
 	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
@@ -1526,10 +1526,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       using_lemmas
       (List.length res_vars)
       hook 
-  with e ->
-    begin
-      (try ignore (Backtrack.backto previous_label) with _ -> ());
-      (*       anomaly (Pp.str "Cannot create termination Lemma") *)
-      raise e
-    end
+  with reraise ->
+    ignore (Backtrack.backto previous_label);
+    (*       anomaly (Pp.str "Cannot create termination Lemma") *)
+    raise reraise
 
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 94b79503a..5ad546588 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -236,7 +236,7 @@ open Format
 
 let getvar lv i =
   try (List.nth lv i)
-  with _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
+  with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
     ^" i="^(string_of_int i)
 
 let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
@@ -589,7 +589,7 @@ let coefpoldep = Hashtbl.create 51
 (* coef of q in p = sum_i c_i*q_i *)
 let coefpoldep_find p q =
   try (Hashtbl.find coefpoldep (p.num,q.num))
-  with _ -> []
+  with Not_found -> []
 
 let coefpoldep_remove p q =
   Hashtbl.remove coefpoldep (p.num,q.num)
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index ce70a0ffb..ca6d305e8 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -163,17 +163,12 @@ let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
 
 (* equality between polynomials *)
 
+exception Failed
+
 let rec equal p q =
   match (p,q) with
       (Pint a,Pint b) -> C.equal a b
-    |(Prec(x,p1),Prec(y,q1)) ->
-       if x<>y then false
-       else if (Array.length p1)<>(Array.length q1) then false
-       else (try (Array.iteri (fun i a -> if not (equal a q1.(i))
-			       then failwith "raté")
-		    p1;
-		  true)
-	     with _ -> false)
+    |(Prec(x,p1),Prec(y,q1)) -> (x=y) && Array.for_all2 equal p1 q1
     | (_,_) -> false
 
 (* normalize polynomial: remove head zeros, coefficients are normalized
@@ -519,12 +514,11 @@ let divP p q=
 
 let div_pol_rat p q=
   let x = max (max_var_pol p) (max_var_pol q) in
-    try (let s = div_pol (multP p (puisP (Pint(coef_int_tete q))
-				     (1+(deg x p) - (deg x q))))
-		   q x in
-         (* degueulasse, mais c 'est pour enlever un warning *)
-         if s==s then true else true)
-    with _ -> false
+  try
+    let r = puisP (Pint(coef_int_tete q)) (1+(deg x p)-(deg x q)) in
+    let _ = div_pol (multP p r) q x in
+    true
+  with Failure _ -> false
 
 (***********************************************************************
   5. Pseudo-division and gcd with subresultants.
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index c16bd4256..d647b14ed 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -26,19 +26,6 @@ let set_of_list_eq eq l =
    List.iter (fun x -> if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l;
    List.rev !res
 
-
-(* Memoization
-   f is compatible with nf: f(nf(x)) = f(x)
-*)
-
-let memos s memoire nf f x =
-   try (let v = Hashtbl.find memoire (nf x) in pr s;v)
-   with _ -> (pr "#";
-	      let v = f x in
-	      Hashtbl.add memoire (nf x) v;
-	      v)
-
-
 (**********************************************************************
   Eléments minimaux pour un ordre partiel de division.
   E est un ensemble, avec une multiplication
diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli
index 83b2ac39b..1f8415752 100644
--- a/plugins/nsatz/utile.mli
+++ b/plugins/nsatz/utile.mli
@@ -10,10 +10,6 @@ val info : string -> unit
 val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
 val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list
 
-(* Memoization *)
-val memos :
-  string -> ('a, 'b) Hashtbl.t -> ('c -> 'a) -> ('c -> 'b) -> 'c -> 'b
-
 
 val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list
 val factorise_tableau :
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 2c41b95f3..60ae0784f 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -220,7 +220,7 @@ let compute_rhs bodyi index_of_f =
 (*s Now the function [compute_ivs] itself *)
 
 let compute_ivs gl f cs =
-  let cst = try destConst f with _ -> i_can't_do_that () in
+  let cst = try destConst f with DestKO -> i_can't_do_that () in
   let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e3674fae0..79db4a9c4 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -247,7 +247,8 @@ let add_equation env e =
 (* accès a une equation *)
 let get_equation env id =
   try Hashtbl.find env.equations id
-  with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e
+  with Not_found as e ->
+    Printf.printf "Omega Equation %d non trouvée\n" id; raise e
 
 (* Affichage des termes réifiés *)
 let rec oprint ch = function
@@ -349,7 +350,8 @@ let rec reified_of_formula env = function
       app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
 
 let reified_of_formula env f =
-  begin try reified_of_formula env f with e -> oprint stderr f; raise e end
+  try reified_of_formula env f
+  with reraise -> oprint stderr f; raise reraise
 
 let rec reified_of_proposition env = function
     Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->
@@ -380,8 +382,8 @@ let rec reified_of_proposition env = function
   | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
 
 let reified_of_proposition env f =
-  begin try reified_of_proposition env f
-  with e -> pprint stderr f; raise e end
+  try reified_of_proposition env f
+  with reraise -> pprint stderr f; raise reraise
 
 (* \subsection{Omega vers COQ réifié} *)
 
@@ -397,11 +399,8 @@ let reified_of_omega env body constant =
   List.fold_right mk_coeff body coeff_constant
 
 let reified_of_omega env body c  =
-  begin try
-    reified_of_omega env body c
-  with e ->
-    display_eq display_omega_var (body,c); raise e
-  end
+  try reified_of_omega env body c
+  with reraise -> display_eq display_omega_var (body,c); raise reraise
 
 (* \section{Opérations sur les équations}
 Ces fonctions préparent les traces utilisées par la tactique réfléchie
@@ -930,8 +929,12 @@ let filter_compatible_systems required systems =
 	if List.mem x required then select l
 	else if List.mem (barre x) required then raise Exit
 	else x :: select l
-    | [] -> [] in
-  List.map_filter (function (sol, splits) -> try Some (sol, select splits) with Exit -> None) systems
+    | [] -> []
+  in
+  List.map_filter
+    (function (sol, splits) ->
+      try Some (sol, select splits) with Exit -> None)
+    systems
 
 let rec equas_of_solution_tree = function
     Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
@@ -1000,10 +1003,11 @@ let rec solve_with_constraints all_solutions path =
   let weighted = filter_compatible_systems path all_solutions in
   let (winner_sol,winner_deps) =
     try select_smaller weighted
-    with e ->
+    with reraise ->
       Printf.printf "%d - %d\n"
 	(List.length weighted) (List.length all_solutions);
-      List.iter display_depend path; raise e in
+      List.iter display_depend path; raise reraise
+  in
   build_tree winner_sol (List.rev path) winner_deps
 
 let find_path {o_hyp=id;o_path=p} env =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index be3817d5e..89e6bf822 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 72de7f471..1396f91d4 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 1ccc10375..fb8a05a97 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