diff options
| author | Gaëtan Gilbert | 2020-02-06 16:07:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | d584d0643e32f2277b1a38ba46fc92993638492b (patch) | |
| tree | 4cbf55a3db010a8eadbb3bd50a01e0ed85eca2ed /plugins/syntax/float_syntax.ml | |
| parent | 34d95672ecace6733d9d2f738ee6d7aee46fb2d0 (diff) | |
unsafe_type_of -> get_type_of in Hipattern.extract_eq_args
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions