Merge branch 'v8.5'

4 files changed, 19 insertions, 26 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e57b48e9e0..6c1f38d48b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -94,7 +94,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
-		     
+
 let unify_resolve poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
@@ -109,21 +109,11 @@ let unify_resolve_gen poly = function
   | Some flags -> unify_resolve poly flags
 
 let exact poly (c,clenv) =
-  let (c, _, _) = c in
-  let ctx, c' = 
-    if poly then
-      let evd', subst = Evd.refresh_undefined_universes clenv.evd in
-      let ctx = Evd.evar_universe_context evd' in
-	ctx, subst_univs_level_constr subst c 
-    else 
-      let ctx = Evd.evar_universe_context clenv.evd in
-	ctx, c
-  in
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let sigma = Sigma.to_evar_map sigma in
-    let sigma = Evd.merge_universe_context sigma ctx in
-    Sigma.Unsafe.of_pair (exact_check c', sigma)
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let clenv', c = connect_hint_clenv poly c clenv gl in
+    Tacticals.New.tclTHEN
+    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+    (exact_check c)
   end }
 
 (* Util *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0fd95aeadb..1608a0ea63 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -22,8 +22,8 @@ val default_search_depth : int ref
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-			 ([ `NF ], 'r) Proofview.Goal.t -> clausenv * constr
-						
+  ('a, 'r) Proofview.Goal.t -> clausenv * constr
+
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2cae9b7946..93c201bf18 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -108,7 +108,7 @@ open Auto
 (***************************************************************************)
 
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
-			  
+
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
@@ -128,11 +128,12 @@ let hintmap_of hdc concl =
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
-  let (c, _, _) = c in
-  let clenv', subst = 
-    if poly then Clenv.refresh_undefined_univs clenv 
-    else clenv, Univ.empty_level_subst
-  in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let clenv', c = connect_hint_clenv poly c clenv gl in
+    Tacticals.New.tclTHEN
+    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+    (e_give_exact c)
+  end }
 
 let rec e_trivial_fail_db db_list local_db =
   let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 95bf1babe0..9527191299 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1096,10 +1096,12 @@ exception Found of constr * types
 
 let prepare_hint check (poly,local) env init (sigma,c) =
   let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
-  (* We re-abstract over uninstantiated evars.
+  (* We re-abstract over uninstantiated evars and universes.
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
-  let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in
+  let sigma, subst = Evd.nf_univ_variables sigma in
+  let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in
+  let c = drop_extra_implicit_args c in
   let vars = ref (collect_vars c) in
   let subst = ref [] in
   let rec find_next_evar c = match kind_of_term c with