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.
---
 tactics/class_tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 82ce2234e3..63cafbf76d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -236,7 +236,7 @@ let with_prods nprods h f =
             f gl (h, diff)
       with e when CErrors.noncritical e ->
         let e, info = Exninfo.capture e in
-        Tacticals.New.tclZEROMSG ~info (CErrors.print e) end
+        Proofview.tclZERO ~info e end
   else Proofview.Goal.enter
          begin fun gl ->
          if Int.equal nprods 0 then f gl (h, None)
-- 
cgit v1.2.3