diff options
| author | Pierre-Marie Pédrot | 2018-11-05 14:15:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 14:15:11 +0100 |
| commit | ebc815989728991850080da0e3033cfabecbb759 (patch) | |
| tree | 8eb9560474fabf5ee81011935747696f05f7b0b1 /kernel/nativelib.ml | |
| parent | 5202b20739d18137780b7729ee657b7eecef5c0c (diff) | |
| parent | 3f22c11c650b6ef7cc0770418255865ebdbfb1ae (diff) | |
Merge PR #8896: Expose Typing.judge_of_apply
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions