diff options
| author | Vincent Semeria | 2020-05-31 09:38:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 20:30:08 +0100 |
| commit | f2a5096bf0829316eba869fe5d929337e6fd8bad (patch) | |
| tree | 5a512b72750bf5121f73886103060f6bdee7c28b /interp/notation_ops.mli | |
| parent | 68bd3b4e3f9932ef4b3f2afd260cec8780ae155f (diff) | |
Improve some error messages.
This also includes aligning with refman when relevant and using capital
letters and final period.
Diffstat (limited to 'interp/notation_ops.mli')
0 files changed, 0 insertions, 0 deletions