diff options
| author | Gabriel Scherer | 2015-06-29 16:24:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 12:57:30 +0200 |
| commit | c11b7c5a34ea16a32a78c796a219d29edd117e74 (patch) | |
| tree | c4dbaefbc0aa3ef9f135f7a86529f2e9b6d7ac28 /kernel/type_errors.mli | |
| parent | ed015ec083e298b2e65b7b61fcf924642d438ee4 (diff) | |
minor: documentation comment for constrintern.ml:sort_fields
(Because the function is private to the module, it is documented in
the .ml rather than the .mli)
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions