diff options
| author | Gaëtan Gilbert | 2020-02-06 20:48:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 4c9649d8ded91774616427dd1f91dec545af9c71 (patch) | |
| tree | f31f2e3f808146d84d41311b31787d2081ede7a5 /kernel/type_errors.ml | |
| parent | 3d0d56f3f0da9d9b459b6178d2afeaf19fda7d41 (diff) | |
unsafe_type_of -> type_of in Cctac (with small refactor)
Not sure if get_type_of would be fine, let's go with this for now.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions