From 70b7aabfdfecfc94fd5cbfd2fbf7b65cfaacdd63 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jul 2020 11:22:20 +0200
Subject: 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.
---
 engine/uState.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'engine/uState.mli')

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
 
-- 
cgit v1.2.3