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 /engine/evd.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 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index c570f75c6b..e85cbc96b2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -987,11 +987,6 @@ let check_constraints evd csts = let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } -let refresh_undefined_universes evd = - let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in - let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in - evd', subst - let nf_univ_variables evd = let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in |