diff options
| author | Gaëtan Gilbert | 2020-02-06 16:10:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 1fd5cec8fbc7323ac7bd710707f37d906c5bc794 (patch) | |
| tree | 02fbaf937d58ac5454b14f139d069460b819fc28 /plugins/syntax/plugin_base.dune | |
| parent | d584d0643e32f2277b1a38ba46fc92993638492b (diff) | |
unsafe_type_of -> get_type_of in Tacticals.general_elim_then_using
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions