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 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/errors.ml')

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