diff options
| author | Gaëtan Gilbert | 2020-02-06 15:06:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | f459030b71fb9bc18fe3b9e9f1c199c4ccd7db09 (patch) | |
| tree | f98207a047253c1b349c74aeedd150c326310b33 /plugins/syntax | |
| parent | 92d34ac2a926ebbe7a1cf339bd3cce0c529a99ec (diff) | |
unsafe_type_of -> type_of in Tactics.find_eliminator
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions