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.
---
 vernac/ppvernac.ml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e0974ac027..b93c920654 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1331,10 +1331,8 @@ let pr_vernac_attributes =
   | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
 
 let pr_vernac ({v = {control; attrs; expr}} as v) =
-  try
-    tag_vernac v
-      (pr_vernac_control control ++
-       pr_vernac_attributes attrs ++
-       pr_vernac_expr expr ++
-       sep_end expr)
-  with e -> CErrors.print e
+  tag_vernac v
+    (pr_vernac_control control ++
+     pr_vernac_attributes attrs ++
+     pr_vernac_expr expr ++
+     sep_end expr)
-- 
cgit v1.2.3