diff options
| author | Maxime Dénès | 2018-09-12 17:25:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-12 17:25:46 +0200 |
| commit | 26936e66c7c16f72fd1a7978505c95af9899ddc0 (patch) | |
| tree | b82a055010d31fd79c7f3b6c69d08011d7b813c0 /kernel/type_errors.ml | |
| parent | 60103f4af881485c0f905ebcb6710b31744466d0 (diff) | |
| parent | 943da5e6fb2412a63d1ea67dfeee635b0b5001f4 (diff) | |
Merge PR #8097: Use more efficient accu check for cofix unfolding in native compilation.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions