From 20f55b720be8018cdf9690d60e4ed05d9c8ad5c3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 25 Jun 2020 20:08:04 +0200
Subject: [exn] Remove some uses of print

Exceptions should not printed except for the top-level.

There is the weird anomaly-absorbing code in `Reductionops`, I wonder
how frequent that case is, but as the exception is absorbed printing
there could have a real impact.
---
 pretyping/reductionops.ml | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6f02d76f3a..cb6e8f086e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1097,12 +1097,17 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
+exception AnomalyInConversion of exn
+
+let _ = CErrors.register_handler (function
+    | AnomalyInConversion e ->
+      Some Pp.(str "Conversion test raised an anomaly:" ++
+               spc () ++ CErrors.print e)
+    | _ -> None)
+
 let report_anomaly (e, info) =
   let e =
-    if is_anomaly e then
-      let msg = Pp.(str "Conversion test raised an anomaly:" ++
-                    spc () ++ CErrors.print e) in
-      UserError (None, msg)
+    if is_anomaly e then AnomalyInConversion e
     else e
   in
   Exninfo.iraise (e, info)
-- 
cgit v1.2.3