diff options
| author | Zeimer | 2018-08-31 09:39:17 +0200 |
|---|---|---|
| committer | Zeimer | 2018-08-31 09:45:17 +0200 |
| commit | d7094a827db14523efe05a1a71cd18f4eb6637ea (patch) | |
| tree | a3185dcbc44a3956b7fc182e14eb3433fd12ddea /kernel/type_errors.mli | |
| parent | a67fa614450467afbd56233f489b2105dc655a58 (diff) | |
Fixed the seealso directive in a few places.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions