Fixing backtrace registering of various tactic-related try-with blocks.

2 files changed, 10 insertions, 9 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b86326dda3..2e54653403 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -69,7 +69,6 @@ module Value = Taccoerce.Value
 let dloc = Loc.ghost
 
 let catching_error call_trace fail e =
-  let e = Errors.push e in
   let inner_trace =
     Option.default [] (Exninfo.get e ltac_trace_info)
   in
@@ -89,7 +88,11 @@ let f_debug : debug_info TacStore.field = TacStore.field ()
 let f_trace : ltac_trace TacStore.field = TacStore.field ()
 
 let catch_error call_trace f x =
-  try f x with e when Errors.noncritical e -> catching_error call_trace raise e
+  try f x
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in
+    catching_error call_trace raise e
+
 let catch_error_tac call_trace tac =
   Proofview.tclORELSE
     tac
@@ -1149,10 +1152,6 @@ and interp_app loc ist fv largs =
               catch_error_tac trace (val_interp ist body)
             end
 	    begin fun e ->
-              (* spiwack: [Errors.push] here is unlikely to do what
-                 it's intended to, or anything meaningful for that
-                 matter. *)
-              let e = Errors.push e in
               Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*>
 	      Proofview.tclZERO e
             end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11ad1aad14..fe3854143c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1096,7 +1096,7 @@ let apply_list = function
 let find_matching_clause unifier clause =
   let rec find clause =
     try unifier clause
-    with exn when catchable_exception exn ->
+    with e when catchable_exception e ->
     try find (clenv_push_prod clause)
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
@@ -1116,6 +1116,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when Errors.noncritical e ->
+    let e = Errors.push e in
     try aux (clenv_push_prod clause)
     with NotExtensibleClause -> raise e
   in
@@ -1130,8 +1131,9 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars id
     try
       let clause = apply_in_once_main flags innerclause (c,lbind) gl in
       clenv_refine_in ~sidecond_first with_evars id clause gl
-    with exn when with_destruct ->
-      descend_in_conjunctions aux (fun _ -> raise exn) c gl
+    with e when with_destruct ->
+      let e = Errors.push e in
+      descend_in_conjunctions aux (fun _ -> raise e) c gl
   in
   aux with_destruct d gl0