From a666788182bce7059e6ba41b917b5ca6ab52ae13 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Jul 2020 19:34:18 +0200
Subject: Code simplification around hint manipulation in Class_tactics.

We inline the clenv universe refreshing, since it was the only place in the
code that used it. Furthermore it was performing useless substitutions in
the clenv.
---
 proofs/clenv.ml  | 10 ----------
 proofs/clenv.mli |  3 ---
 2 files changed, 13 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 9bd7ccda5d..db76d08736 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -47,16 +47,6 @@ let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv
 let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval
 let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp
 
-let refresh_undefined_univs clenv =
-  match EConstr.kind clenv.evd clenv.templval.rebus with
-  | Var _ -> clenv, Univ.empty_level_subst
-  | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
-  | _ ->
-    let evd', subst = Evd.refresh_undefined_universes clenv.evd in
-    let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
-      { clenv with evd = evd'; templval = map_freelisted clenv.templval;
-        templtyp = map_freelisted clenv.templtyp }, subst
-
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
 let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index fd1e2fe593..43e808dac7 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -45,9 +45,6 @@ val mk_clenv_from_n :
   Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
-(** Refresh the universes in a clenv *)
-val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
-
 (** {6 linking of clenvs } *)
 
 val clenv_fchain :
-- 
cgit v1.2.3