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

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

7 files changed, 22 insertions, 21 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 92ee55e433..fff4f67b12 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
   let sigma',typed_c =
     try Pretyping.understand_ltac ~resolve_classes:true true 
       sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc
-    with _ ->
+    with e when Errors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 42dcbd1929..7948020a9e 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -275,7 +275,7 @@ let check_typability env sigma c =
 
 let recheck_typability (what,id) env sigma t =
   try check_typability env sigma t
-  with _ ->
+  with e when Errors.noncritical e ->
     let s = match what with
       | None -> "the conclusion"
       | Some id -> "hypothesis "^(Names.Id.to_string id) in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e2f698acd3..90014835b9 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -100,7 +100,7 @@ let clear_hyps sigma ids sign cl =
 
 let recheck_typability (what,id) env sigma t =
   try check_typability env sigma t
-  with _ ->
+  with e when Errors.noncritical e ->
     let s = match what with
       | None -> "the conclusion"
       | Some id -> "hypothesis "^(Id.to_string id) in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 961ff41fb7..d8609ed80f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -55,10 +55,10 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
    | None -> Proofview.tclUNIT ()
   in
   try Proof_global.run_tactic tac
-  with e ->
-    let e = Errors.push e in
+  with reraise ->
+    let reraise = Errors.push reraise in
     Proof_global.discard_current ();
-    raise e
+    raise reraise
 
 let restart_proof () = undo_todepth 1
 
@@ -154,9 +154,9 @@ let build_constant_by_tactic id sign typ tac =
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
     delete_current_proof ();
     const
-  with e ->
+  with reraise ->
     delete_current_proof ();
-    raise e
+    raise reraise
 
 let build_by_tactic env typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 479ccabccb..d3c3fb71a7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -321,7 +321,7 @@ let rec rollback pr =
 let transaction pr t =
   init_transaction pr;
   try t (); commit pr
-  with e -> rollback pr; raise e
+  with reraise -> rollback pr; raise reraise
 
 
 (* Focus command (focuses on the [i]th subgoal) *)
@@ -416,9 +416,9 @@ let run_tactic env tac pr =
     let tacticced_proofview = Proofview.apply env tac sp in
     pr.state <- { pr.state with proofview = tacticced_proofview };
     push_undo starting_point pr
-  with e -> 
+  with reraise ->
     restore_state starting_point pr;
-    raise e
+    raise reraise
 
 (*** Commands ***)
 
@@ -463,7 +463,7 @@ module V82 = struct
 	let new_proofview = Proofview.V82.instantiate_evar n com sp in
 	pr.state <- { pr.state with proofview = new_proofview };
 	push_undo starting_point pr
-      with e -> 
+      with reraise ->
 	restore_state starting_point pr;
-	raise e
+	raise reraise
 end
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 4592c60dd7..04d1258047 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -231,7 +231,7 @@ let tclORELSE0 t1 t2 g =
   try
     t1 g
   with (* Breakpoint *)
-    | e -> catch_failerror e; t2 g
+    | e when Errors.noncritical e -> catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
@@ -243,7 +243,7 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
-    with e -> catch_failerror e; None
+    with e when Errors.noncritical e -> catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
@@ -274,7 +274,7 @@ let ite_gen tcal tac_if continue tac_else gl=
     try
       tcal tac_if0 continue gl
     with (* Breakpoint *)
-      | e -> catch_failerror e; tac_else0 e gl
+      | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl
 
 (* Try the first tactic and, if it succeeds, continue with
    the second one, and if it fails, use the third one *)
@@ -328,7 +328,7 @@ let tclTIMEOUT n t g =
     | TacTimeout ->
       restore_timeout ();
       errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!")
-    | e -> restore_timeout (); raise e
+    | reraise -> restore_timeout (); raise reraise
 
 (* Beware: call by need of CAML, g is needed *)
 let rec tclREPEAT t g =
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 5952fd29cb..8ad92910f3 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -142,11 +142,12 @@ let debug_prompt lev g tac f =
     else (decr skip; run false; if Int.equal !skip 0 then skipped:=0; DebugOn (lev+1)) in
   (* What to execute *)
   try f newlevel
-  with e ->
+  with reraise ->
     skip:=0; skipped:=0;
-    if Logic.catchable_exception e then
-      msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
-    raise e
+    if Logic.catchable_exception reraise then
+      msg_tac_debug
+        (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise);
+    raise reraise
 
 let is_debug db = match db, !breakpoint with
 | DebugOff, _ -> false