Updated version 8.9.0 from 'upstream/8.9.0'

with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63

1 files changed, 3 insertions, 6 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0c0d9bcf..d7de6c4f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -8,8 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-module CVars = Vars
-
 open Pp
 open Util
 open Names
@@ -81,15 +79,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
   let clenv, c =
     if poly then
       (** Refresh the instance of the hint *)
-      let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
-      let map c = CVars.subst_univs_level_constr subst c in
+      let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
       let emap c = Vars.subst_univs_level_constr subst c in
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       (** Only metas are mentioning the old universes. *)
       let clenv = {
         templval = Evd.map_fl emap clenv.templval;
         templtyp = Evd.map_fl emap clenv.templtyp;
-        evd = Evd.map_metas map evd;
+        evd = Evd.map_metas emap evd;
         env = Proofview.Goal.env gl;
       } in
       clenv, emap c
@@ -102,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
-  Clenvtac.clenv_refine false clenv
+  Clenvtac.clenv_refine clenv
   end
 
 let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h