diff options
| author | Pierre-Marie Pédrot | 2020-07-17 11:22:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | 70b7aabfdfecfc94fd5cbfd2fbf7b65cfaacdd63 (patch) | |
| tree | 11604a251fdef86e5482cb016946c813d226796a /plugins/syntax/float_syntax.ml | |
| parent | 2e22662662ebb44a18b8950e3b2876d6787d2d2f (diff) | |
Remove dead code after the previous commit.
The costly universe refreshing functions were only used for typeclass hint
resolution, which now relies on the provided hint context.
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions