From 2f8bc98ab583a7259e167cd6bf3bce36aa33ada6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 14 Mar 2013 17:43:06 +0000
Subject: Embedded exns in LtacLocated and EvaluatedError satisfy
 Errors.noncritical

 This was apparently already the case before, but this invariant is now
 explicited in comments + a few asserts.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16305 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/errors.ml  | 4 ----
 lib/errors.mli | 4 ----
 2 files changed, 8 deletions(-)

(limited to 'lib')

diff --git a/lib/errors.ml b/lib/errors.ml
index 157949fcd9..ae188cfeb2 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -110,10 +110,6 @@ let print_no_report e = print_gen (print_anomaly false) !handle_stack e
 
 let print_anomaly e = print_anomaly true e
 
-(** Same as [print], except that anomalies are not printed but re-raised
-    (used for the Fail command) *)
-let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
-
 (** Predefined handlers **)
 
 let _ = register_handler begin function
diff --git a/lib/errors.mli b/lib/errors.mli
index c5400574b8..a7f4ef0cdf 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -81,10 +81,6 @@ val print_anomaly : exn -> Pp.std_ppcmds
     isn't printed (used in Ltac debugging). *)
 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
-
 (** Critical exceptions shouldn't be catched and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user.
-- 
cgit v1.2.3