Fixing various backtrace recordings.

5 files changed, 22 insertions, 29 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 632f83c83..152556c74 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1205,6 +1205,7 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
 	  out
 	with reraise ->
+          let reraise = Errors.push reraise in
 	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
 	  raise reraise
       end
@@ -1216,6 +1217,7 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  trace := (depth, Some pp) :: !trace;
 	  out
 	with reraise ->
+          let reraise = Errors.push reraise in
 	  trace := (depth, None) :: !trace;
 	  raise reraise
       end
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9c8412454..f245247a9 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -90,25 +90,23 @@ let contradiction_term (c,lbind as cl) =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_type_of gl in
-    try (* type_of can raise exceptions. *)
-      let typ = type_of c in
-      let _, ccl = splay_prod env sigma typ in
-      if is_empty_type ccl then
-        Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
-      else
-        Proofview.tclORELSE
-          begin
-            if lbind = NoBindings then
-	      filter_hyp (is_negation_of env sigma typ)
-	        (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
-            else
-	      Proofview.tclZERO Not_found
-          end
-          begin function
-            | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
-            | e -> Proofview.tclZERO e
-          end
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let typ = type_of c in
+    let _, ccl = splay_prod env sigma typ in
+    if is_empty_type ccl then
+      Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
+    else
+      Proofview.tclORELSE
+        begin
+          if lbind = NoBindings then
+            filter_hyp (is_negation_of env sigma typ)
+              (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
+          else
+            Proofview.tclZERO Not_found
+        end
+        begin function
+          | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+          | e -> Proofview.tclZERO e
+        end
   end
 
 let contradiction = function
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 71b3c0045..c59e43b45 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -387,11 +387,6 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
             end
             begin function
               | e ->
-                  (* Try to see if there's an equality hidden *)
-                  (* 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
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
 	          match match_with_equality_type t' with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7c460424e..b3f33b19c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1258,10 +1258,6 @@ and interp_match ist lz constr lmr gl =
     (interp_ltac_constr ist constr gl)
     begin function
       | 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 true e
           (fun () -> str "evaluation of the matched expression")) <*>
           Proofview.tclZERO e
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9c2a1f6e3..3dd208acb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3657,11 +3657,13 @@ let abstract_subproof id tac =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
   let (const, safe) =
     try Pfedit.build_constant_by_tactic id secsign concl solve_tac
-    with Proof_errors.TacticFailure e ->
+    with Proof_errors.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
        means that [e] comes from [tac] failing to yield enough
        success). Hence it reraises [e]. *)
+    let src = Errors.push src in
+    let e = Backtrace.app_backtrace ~src ~dst:e in
     raise e
   in
   let cd = Entries.DefinitionEntry const in