diff options
| author | Jason Gross | 2020-08-30 15:48:04 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-08-30 15:48:04 -0400 |
| commit | 921a56a0500651323db9541dea9d195d84776fd2 (patch) | |
| tree | 181932b6eb955f577ad7c6e77b29aff16b7bcbdc /kernel/type_errors.mli | |
| parent | 94d9fe2b6cb06fe7f862683d8337433e18314001 (diff) | |
Fix rendering of -> in micromega
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions