diff options
| author | Gaëtan Gilbert | 2020-02-06 20:16:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 791797fce5e11b83b88e6b869678ee7c39703043 (patch) | |
| tree | ad542f031d039da441d08e211ab97d3d4d4f61ad /kernel/nativecode.ml | |
| parent | 2e1c1bc858780a79b4196528500dda4117d4cfba (diff) | |
unsafe_type_of -> type_of in Rewrite.resolve_morphism
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions