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 -----
 engine/evd.mli    |  2 --
 engine/uState.ml  | 29 -----------------------------
 engine/uState.mli |  2 --
 4 files changed, 38 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
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
 
diff --git a/engine/uState.ml b/engine/uState.ml
index d4cb59da26..ca0a21acf7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -718,35 +718,6 @@ let fix_undefined_variables uctx =
   { uctx with univ_variables = vars';
     univ_algebraic = algs' }
 
-let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in
-  let subst_fn u = subst_univs_level_level subst u in
-  let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc)
-    uctx.univ_algebraic LSet.empty
-  in
-  let vars =
-    LMap.fold
-      (fun u v acc ->
-        LMap.add (subst_fn u)
-          (Option.map (subst_univs_level_universe subst) v) acc)
-      uctx.univ_variables LMap.empty
-  in
-  let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in
-  let lbound = uctx.universes_lbound in
-  let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g)
-      (ContextSet.levels ctx') g in
-  let initial = declare uctx.initial_universes in
-  let univs = declare UGraph.initial_universes in
-  let uctx' = {names = uctx.names;
-               local = ctx';
-               seff_univs = uctx.seff_univs;
-               univ_variables = vars; univ_algebraic = alg;
-               universes = univs;
-               universes_lbound = lbound;
-               initial_universes = initial;
-               weak_constraints = weak; } in
-    uctx', subst
-
 let minimize uctx =
   let open UnivMinim in
   let lbound = uctx.universes_lbound in
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