From 2800a82dec607120fd2a378f7ac3bf4d6e8df18c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 2 Feb 2014 17:59:39 +0100
Subject: Fixing backtrace reporting.

---
 proofs/proofview_gen.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'proofs')

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 = 
-- 
cgit v1.2.3