diff options
| author | Hugo Herbelin | 2021-04-04 04:43:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-08 17:35:42 +0200 |
| commit | 4c3247586a86ff528d9eee6d8a1c8266f3d3fca1 (patch) | |
| tree | db19e4a19945deeb1678b41757e209f32dd0229f /kernel/type_errors.mli | |
| parent | 8716a37faeff72a38aae5cf5b6835ceab470e95c (diff) | |
Gramlib: some comments about how new rules are inserted.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions