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 /_CoqProject | |
| 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 '_CoqProject')
0 files changed, 0 insertions, 0 deletions