Fixing backtrace reporting.

2 files changed, 22 insertions, 4 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index b4935cc680..a160aaa87e 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -213,7 +213,12 @@ Module IOBase.
  Extract Constant raise => "fun e -> (); fun () -> raise (Proof_errors.Exception e)".
  Extraction Implicit raise [A].
  Parameter catch : forall A, T A -> (Exception -> T A) -> T A.
- Extract Constant catch => "fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> let e = Errors.push e in h e ()".
+ Extract Constant catch => "fun s h -> ();
+  fun () -> try s ()
+  with Proof_errors.Exception e as src ->
+    let src = Errors.push src in
+    let e = Backtrace.app_backtrace ~src ~dst:e in
+    h e ()".
  Extraction Implicit catch [A].
 
  Parameter read_line : T String.
@@ -652,7 +657,11 @@ Module NonLogical.
 
  (* /!\ The extracted code for [run] performs effects. /!\ *)
  Parameter run : forall a:Set, t a -> a.
- Extract Constant run => "fun x -> try x () with Proof_errors.Exception e -> let e = Errors.push e in Pervasives.raise e".
+ Extract Constant run => "fun x ->
+  try x () with Proof_errors.Exception e as src ->
+    let src = Errors.push src in
+    let e = Backtrace.app_backtrace ~src ~dst:e in
+    Pervasives.raise e".
  Extraction Implicit run [a].
 
 End NonLogical.
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 90266c6d09..92012d58b1 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -49,7 +49,12 @@ module IOBase =
   
   (** val catch : 'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1 coq_T **)
   
-  let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> let e = Errors.push e in h e ()
+  let catch = fun s h -> ();
+  fun () -> try s ()
+  with Proof_errors.Exception e as src ->
+    let src = Errors.push src in
+    let e = Backtrace.app_backtrace ~src ~dst:e in
+    h e ()
   
   (** val read_line : string coq_T **)
   
@@ -167,7 +172,11 @@ module NonLogical =
   
   (** val run : 'a1 t -> 'a1 **)
   
-  let run = fun x -> try x () with Proof_errors.Exception e -> let e = Errors.push e in Pervasives.raise e
+  let run = fun x ->
+  try x () with Proof_errors.Exception e as src ->
+    let src = Errors.push src in
+    let e = Backtrace.app_backtrace ~src ~dst:e in
+    Pervasives.raise e
  end
 
 module Logical =