diff options
| author | Théo Zimmermann | 2018-08-01 10:53:25 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-01 10:53:25 +0200 |
| commit | 29a432dfbaa83dd1459c7af95f556555da15a1ce (patch) | |
| tree | 481e7fdf9756f595c7ef10a5702199ca3fc13761 /kernel/type_errors.ml | |
| parent | e130be4ccb68e0876ed789d295ae9a94d4358bf9 (diff) | |
| parent | acc7acfa0e8015b5785cb0f2d01acca2448e8197 (diff) | |
Merge PR #8195: Fix doc for no associativity
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions