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/evd.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'engine/evd.ml')

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