diff options
| author | Gaëtan Gilbert | 2020-02-06 20:29:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | aa0f5e5cf23a650bf0302d2c35aa2b0d56f59f48 (patch) | |
| tree | 69d4d427406c5df7b39392580d03d874dd410d11 /plugins/syntax/string_notation.mli | |
| parent | b0b473f5867d216b815dd1acb1b4da2e794d1095 (diff) | |
unsafe_type_of -> get_type_of in Extractactics.mkCaseEq
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions