diff options
| author | Hugo Herbelin | 2019-11-12 10:57:52 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-19 21:02:02 +0100 |
| commit | 5baa841738e60eee65ffc9e313e7cae6f03032e1 (patch) | |
| tree | 867fc270d8f4d9f33b8070bcc5adc60ef82085d7 /kernel/names.ml | |
| parent | 11aa34ba3f40256ed920419d503393aca349a131 (diff) | |
G_constr: Uniformization of indentation.
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions