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

3 files changed, 34 insertions, 13 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