diff options
| author | Gaëtan Gilbert | 2020-02-06 15:09:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 2397d52d8e2f337ffd53d1198b21bb882b52d8a8 (patch) | |
| tree | c519959c6b8554300351ee33ff04024c4f688b75 /tactics/hipattern.ml | |
| parent | f459030b71fb9bc18fe3b9e9f1c199c4ccd7db09 (diff) | |
unsafe_type_of -> type_of in Tactics.cut_and_apply
Diffstat (limited to 'tactics/hipattern.ml')
0 files changed, 0 insertions, 0 deletions