aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-06-25 20:08:04 +0200
committerEmilio Jesus Gallego Arias2020-07-09 19:39:47 +0200
commit20f55b720be8018cdf9690d60e4ed05d9c8ad5c3 (patch)
tree98ea37269ad171112a44421d363f354205c49a5b /vernac
parent577ec77f17a872d6bc36073ceeb3cf582fcf01c4 (diff)
[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.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/ppvernac.ml12
1 files changed, 5 insertions, 7 deletions
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)