diff options
| author | Lasse Blaauwbroek | 2020-12-22 06:15:28 +0100 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-12-27 18:26:01 +0100 |
| commit | d1af000c4b9b1d1ff9b2f9fbf2dcb570ae7c974c (patch) | |
| tree | 6ee84b6104fdfacab5a63661b8577a079cc72a3e /kernel/type_errors.ml | |
| parent | a84ff9806f0ee77e081954453ee6afb67921eb50 (diff) | |
Make ssrtermkind algebraic instead of a char
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions