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.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'lib/errors.mli') diff --git a/lib/errors.mli b/lib/errors.mli index 03caa6a9f..5bd572474 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