diff options
| author | Gaëtan Gilbert | 2020-12-01 11:53:36 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-12-01 11:53:36 +0100 |
| commit | baaa28f921e8ed2045acb14da94f2c8e1701fa1f (patch) | |
| tree | 3ba98e0c5cd3c60a3b1ffdf962df6dec9448c153 /kernel/type_errors.ml | |
| parent | 36e2df30d23d56f0a80adcd3ed5c04d64117af74 (diff) | |
Added comment about l2r in check_correct_arity
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions