diff options
| author | Alasdair Armstrong | 2018-12-26 20:42:54 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-26 20:42:54 +0000 |
| commit | 25a8a48142cc715c55f11fc80cf3dad6bec1b71d (patch) | |
| tree | a5bd2ab3fc8a9b6893fec5dbdf06ea42428be53b /src/error_format.ml | |
| parent | bd6c099d7b541c7850e98347c6bfce743ca11434 (diff) | |
More cleanup
Remove unused name schemes and DEF_kind
Diffstat (limited to 'src/error_format.ml')
0 files changed, 0 insertions, 0 deletions