diff options
| author | Emilio Jesus Gallego Arias | 2020-06-25 20:08:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-09 19:39:47 +0200 |
| commit | 20f55b720be8018cdf9690d60e4ed05d9c8ad5c3 (patch) | |
| tree | 98ea37269ad171112a44421d363f354205c49a5b /vernac | |
| parent | 577ec77f17a872d6bc36073ceeb3cf582fcf01c4 (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.ml | 12 |
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) |
