diff options
| author | Gaëtan Gilbert | 2020-02-06 16:13:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 5a2600f47b64495a8754be74f3156f915a2497ec (patch) | |
| tree | 5a43ac5a7f7fccdee7062a9bed372d27996c818b /plugins/syntax/plugin_base.dune | |
| parent | 598558339afec652467c78d0bd6e472df051ef69 (diff) | |
unsafe_type_of -> get_type_of in Class_tactics.autoapply
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions