diff options
| author | Emilio Jesus Gallego Arias | 2020-11-16 16:18:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-18 16:25:00 +0100 |
| commit | efa6673158f5eaa3fc11c0b3d1e3285c4acc129a (patch) | |
| tree | 79d8b3cccd9759fc63cf22998e191928870e6993 /interp/notation_ops.ml | |
| parent | 6aeee2e4e37d4b8ffb8c50c109903ad336c8bdfa (diff) | |
[attributes] Add output test suite for errors, improve error printing.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions