Fixing backtrace handling here and there.

1 files changed, 10 insertions, 7 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 6cf0b1396..b4935cc68 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -213,15 +213,15 @@ 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 -> h e ()".
+ Extract Constant catch => "fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> let e = Errors.push e in h e ()".
  Extraction Implicit catch [A].
 
  Parameter read_line : T String.
- Extract Constant read_line => "fun () -> try Pervasives.read_line () with e -> raise e ()".
+ Extract Constant read_line => "fun () -> try Pervasives.read_line () with e -> let e = Errors.push e in raise e ()".
  Parameter print_char : Char -> T unit.
  Extract Constant print_char => "fun c -> (); fun () -> print_char c".
  Parameter print : Ppcmds -> T unit.
- Extract Constant print => "fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()".
+ Extract Constant print => "fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> let e = Errors.push e in raise e ()".
 
  Parameter timeout: forall A, Int -> T A -> T A.
  Extract Constant timeout => "fun n t -> (); fun () ->
@@ -237,7 +237,10 @@ Module IOBase.
       restore_timeout ();
       res
     with
-    | e -> restore_timeout (); Pervasives.raise e
+    | e ->
+      let e = Errors.push e in
+      restore_timeout ();
+      Pervasives.raise e
  ".
  Extraction Implicit timeout [A].
 
@@ -649,7 +652,7 @@ 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 -> Pervasives.raise e".
+ Extract Constant run => "fun x -> try x () with Proof_errors.Exception e -> let e = Errors.push e in Pervasives.raise e".
  Extraction Implicit run [a].
 
 End NonLogical.
@@ -694,9 +697,9 @@ End Logical.
 Set Extraction Flag 1007.
 Set Extraction Conservative Types.
 Set Extraction File Comment "
-This file has been generated by extraction of bootstrap/Monad.v.
+This file has been generated by extraction of bootstrap/Monads.v.
 It shouldn't be modified directly. To regenerate it run
-coqtop -batch -impredicative-set -l bootstrap/Monad.v in Coq's source
+coqtop -batch -impredicative-set -l bootstrap/Monads.v in Coq's source
 directory.
 ".