diff options
| author | Gaëtan Gilbert | 2020-02-06 17:55:30 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | bab30bf5d6aa2196508bf939dd8d1b0c82140ffb (patch) | |
| tree | fd556bf7ef2b8d8df8df8fc9636b0045487c95d1 /kernel/nativecode.ml | |
| parent | af788fd0daeed459b98ed9acd3a0443f53666176 (diff) | |
unsafe_type_of -> get_type_of in Firstorded.Instances.mk_open_instance
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions