From 0892990d7bbeb770de458a3b4ef2ffe34a1b11e3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 28 Jan 2013 21:06:02 +0000
Subject: Actually adding backtrace handling.

I hope I did not forget some [with] clauses. Otherwise, some
stack frame will be missing from the debug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/errors.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'lib/errors.mli')

diff --git a/lib/errors.mli b/lib/errors.mli
index 00c39c2b3d..d596abb55a 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -11,6 +11,14 @@ open Pp
 (** This modules implements basic manipulations of errors for use
     throughout Coq's code. *)
 
+(** {6 Error handling} *)
+
+val push : exn -> exn
+(** Alias for [Backtrace.push_exn]. *)
+
+val reraise : exn -> 'a
+(** Alias for [Backtrace.reraise]. *)
+
 (** {6 Generic errors.}
 
  [Anomaly] is used for system errors and [UserError] for the
@@ -85,3 +93,6 @@ val print_no_report : exn -> Pp.std_ppcmds
 (** Same as [print], except that anomalies are not printed but re-raised
     (used for the Fail command) *)
 val print_no_anomaly : exn -> Pp.std_ppcmds
+
+(** Enable registering of backtrace information. *)
+val record_backtrace : unit -> unit
-- 
cgit v1.2.3