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

3 files changed, 23 insertions, 16 deletions

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 =