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.

3 files changed, 10 insertions, 16 deletions

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 :
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6c1bdca682..279476badb 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -143,6 +143,12 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
     resolve_evars = false
 }
 
+let refresh_undefined_univs clenv =
+  match EConstr.kind clenv.evd clenv.templval.rebus with
+  | Var _ -> clenv.evd, Univ.empty_level_subst
+  | App (f, args) when isVar clenv.evd f -> clenv.evd, Univ.empty_level_subst
+  | _ -> Evd.refresh_undefined_universes clenv.evd
+
 let e_give_exact flags h =
   let { hint_term = c; hint_clnv = clenv } = h in
   let open Tacmach.New in
@@ -150,8 +156,9 @@ let e_give_exact flags h =
   let sigma = project gl in
   let c, sigma =
     if h.hint_poly then
-      let clenv', subst = Clenv.refresh_undefined_univs clenv in
-      let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
+      (* Should we really refresh all universes when we have the local ones at hand? *)
+      let evd, subst = refresh_undefined_univs clenv in
+      let evd = evars_reset_evd ~with_conv_pbs:true sigma evd in
       let c = Vars.subst_univs_level_constr subst c in
         c, evd
     else c, sigma
@@ -224,7 +231,7 @@ let unify_resolve_refine flags h diff =
 let with_prods nprods h f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
-      let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
+      let { hint_term = c; hint_poly = poly } = h in
       if poly || Int.equal nprods 0 then f None
       else
         let sigma = Tacmach.New.project gl in