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.mli | |
| 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.mli')
| -rw-r--r-- | engine/evd.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 679173ca72..3f17e63034 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -643,8 +643,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val fix_undefined_variables : evar_map -> evar_map -val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst - (** Universe minimization *) val minimize_universes : evar_map -> evar_map |