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/uState.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/uState.mli')
| -rw-r--r-- | engine/uState.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/engine/uState.mli b/engine/uState.mli index 45a0f9964e..607c6c9452 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -154,8 +154,6 @@ val abstract_undefined_variables : t -> t val fix_undefined_variables : t -> t -val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst - (** Universe minimization *) val minimize : t -> t |