diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-06 19:13:14 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-09 23:53:21 +0100 |
| commit | dcd2cd38fe633652cd67707a8e5f9a8a0c8ca74b (patch) | |
| tree | edfd3affde6ce6dae6049240d51ec2462e641c6b /vernac/topfmt.ml | |
| parent | 33789b2d1706194d478a25098bd1991d2c845223 (diff) | |
[vernac] [minor] Move print effects to top-level caller.
We remove many individual calls to `msg_notice` in the print
vernacular dispatcher in favor of a single, top-level calls.
This is a minor refactoring but will help in handling `Print Foo` more uniformly.
Diffstat (limited to 'vernac/topfmt.ml')
0 files changed, 0 insertions, 0 deletions