diff options
| author | Regis-Gianas | 2014-11-04 23:04:30 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 23:04:39 +0100 |
| commit | 3b9ab8c8f596a66bf38b672d7e8cf32db3b08577 (patch) | |
| tree | 93fc4a0cf688efcb07c508a647592f17b69a7e77 /kernel/type_errors.ml | |
| parent | d1569f060a114b113ea9f326f1dec1c1e3f101dc (diff) | |
lib/richPp: Cosmetics.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions