diff options
| author | Gaëtan Gilbert | 2020-02-06 15:55:29 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 276aa928c9b3c2337aebf21383e18f145735426b (patch) | |
| tree | 6dfc4404d543d5b532b503089f1369b074a005fb /plugins/syntax/string_notation.ml | |
| parent | a9e4f78935ba091d7e012df8398bccc5d08d1370 (diff) | |
unsafe_type_of -> get_type_of in Tactics.is_functional_induction
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions