From 2a5fd12d597d4337810ae367ea3a49720ee3d80c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 21 Apr 2015 17:43:01 +0200
Subject: STM: print trace on "anomaly, no safe id attached"

---
 lib/errors.ml  | 2 ++
 lib/errors.mli | 1 +
 2 files changed, 3 insertions(+)

(limited to 'lib')

diff --git a/lib/errors.ml b/lib/errors.ml
index a4ec357ee4..13f3916477 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -99,6 +99,8 @@ let iprint (e, info) = print ~info e
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+let iprint_no_report (e, info) =
+  print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info
 
 (** Predefined handlers **)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index 03caa6a9f8..5bd5724746 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -80,6 +80,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
+val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds
 
 (** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
-- 
cgit v1.2.3