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

5 files changed, 44 insertions, 22 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 9e6045661..aafacaeb3 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -326,11 +326,9 @@ module V82 = struct
       { p with proofview = Proofview.V82.grab p.proofview }
 
 
-    let instantiate_evar n com pr =
-      let sp = pr.proofview in
-      try
-	let new_proofview = Proofview.V82.instantiate_evar n com sp in
-        { pr with proofview = new_proofview }
-      with e ->
-	raise e
+  let instantiate_evar n com pr =
+    let sp = pr.proofview in
+    let new_proofview = Proofview.V82.instantiate_evar n com sp in
+    { pr with proofview = new_proofview }
+
 end
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 1dff6203b..a0c64d29d 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -529,6 +529,7 @@ let tclSENSITIVE s =
     let next = sensitive_on_proofview s env step in
     Proof.set next
   with e when catchable_exception e ->
+    let e = Errors.push e in
     tclZERO e
 
 let tclPROGRESS t =
@@ -691,6 +692,7 @@ module V82 = struct
       let sgs = List.flatten goalss in
       Proof.set { ps with solution=evd ; comb=sgs; }
     with e when catchable_exception e ->
+      let e = Errors.push e in
       tclZERO e
 
 
@@ -762,7 +764,9 @@ module V82 = struct
       let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
       let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
-    with Proof_errors.TacticFailure e -> raise e
+    with Proof_errors.TacticFailure e ->
+      let e = Errors.push e in
+      raise e
 
   let put_status b =
     Proof.put (b,([],[]))
@@ -801,6 +805,7 @@ module Goal = struct
       Proof.set { step with solution=sigma } >>
         Proof.ret res
     with e when catchable_exception e ->
+      let e = Errors.push e in
       tclZERO e
 
   let return x = lift (Goal.return x)
@@ -817,6 +822,7 @@ module Goal = struct
         let (t,_) = Goal.eval (enter_t f) env sigma goal in
         t
       with e when catchable_exception e ->
+        let e = Errors.push e in
         tclZERO e
     end
   let enterl f =
@@ -829,6 +835,7 @@ module Goal = struct
         t >= fun r ->
         tclUNIT (r::acc)
       with e when catchable_exception e ->
+        let e = Errors.push e in
         tclZERO e
     end >= fun res ->
     tclUNIT (List.flatten (List.rev res))
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index f6ba5341e..e1815cca9 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -20,13 +20,25 @@ let get = fun r -> (); fun () -> Pervasives.(!) r
 
 let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
 
-let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()
-
-let read_line = fun () -> try Pervasives.read_line () with e -> raise e ()
+let catch = fun s h -> (); fun () ->
+  try s ()
+  with Proof_errors.Exception e ->
+    let e = Errors.push e in
+    h e ()
+
+let read_line = fun () ->
+  try Pervasives.read_line ()
+  with e ->
+    let e = Errors.push e in
+    raise e ()
 
 let print_char = fun c -> (); fun () -> print_char c
 
-let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
+let print = fun s -> (); fun () ->
+  try Pp.pp s; Pp.pp_flush ()
+  with e ->
+    let e = Errors.push e in
+    raise e ()
 
 let timeout = fun n t -> (); fun () ->
   let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
@@ -43,7 +55,11 @@ let timeout = fun n t -> (); fun () ->
   with
   | e -> restore_timeout (); Pervasives.raise e
 
-let run = fun x -> try x () with Proof_errors.Exception e -> Pervasives.raise e
+let run x =
+  try x ()
+  with Proof_errors.Exception e ->
+    let e = Errors.push e in
+    Pervasives.raise e
 
 end
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b86326dda..2e5465340 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 11ad1aad1..fe3854143 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