diff options
| author | Gaëtan Gilbert | 2020-02-06 20:28:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | b0b473f5867d216b815dd1acb1b4da2e794d1095 (patch) | |
| tree | fae9c97aa360d85f979ee6579cc3a8c2170ec305 /plugins/syntax/string_notation.mli | |
| parent | 6283c94c640d6b1f911b644583ee656a7a8b9a1f (diff) | |
unsafe_type_of -> get_type_of in Rewrite.symmetry_in
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions