diff options
| author | Pierre-Marie Pédrot | 2020-07-18 11:34:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-18 11:34:12 +0200 |
| commit | e6d92a9765f84c80f8c6a102fe5480490c747313 (patch) | |
| tree | ee51e80ca8001dbad69cc93d2d8e97b826eb2cc6 /vernac | |
| parent | 689a391bddb956fdc05ec267866ef2253c731cc3 (diff) | |
| parent | d2ca1efe969ece40254ba19281964c7f391f3f99 (diff) | |
Merge PR #12588: [exn] Remove some uses of print
Ack-by: gares
Reviewed-by: ppedrot
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) |
