diff options
| author | Pierre-Marie Pédrot | 2020-09-02 18:07:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-02 18:08:58 +0200 |
| commit | 93ac07bbb48ba3a2eca0d5c75aa9be7095a19912 (patch) | |
| tree | b21c5acb87a9330243f73a52bcca1ad72a9bdd72 /kernel/type_errors.mli | |
| parent | 8f484215c8f9beddeffbf0787dbd23265dddfc29 (diff) | |
Document the Equality.equality type in the ML file.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions