diff options
| author | Théo Zimmermann | 2019-10-30 17:10:05 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-10-30 17:19:57 +0100 |
| commit | fa822f0762df1c46d8e179afb9b408a927fff149 (patch) | |
| tree | 145cfc25bff38d747437750ce31f2de288a77dde /kernel/type_errors.ml | |
| parent | 5d1f7461f74f727d0394e904c3ee820134b22c64 (diff) | |
Use bullets and indentation (but the result rendering is weird).
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions