Univs/(e)auto: fix bug #4450 polymorphic exact hints

The exact and e_exact tactics were not registering the universes and
constraints of the hint correctly. Now using the same connect_hint_clenv
as unify_resolve, they do. Also correct the implementation of
prepare_hint to normalize the universes of the hint before abstracting
its undefined universes. They are going to be refreshed at each
application. This means that eauto using term can
use multiple different instantiations of the universes of term
if term introduces new universes. If we want just one instantiation
then the term should be abbreviated in the goal first.

5 files changed, 81 insertions, 26 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 647ff9714..45da04cf0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -97,7 +97,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 begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
@@ -112,19 +112,12 @@ 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.enter begin fun gl ->
-    let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
-    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c')
+  Proofview.Goal.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 2e5647f87..0276e8258 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -26,8 +26,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 ] Proofview.Goal.t -> clausenv * constr
-						
+			 'a Proofview.Goal.t -> clausenv * constr
+
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 568b1d17c..cb206a7dd 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -117,7 +117,7 @@ open Unification
 (***************************************************************************)
 
 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 begin
       fun gl ->
@@ -138,12 +138,14 @@ 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 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))
+    (Proofview.V82.tactic (e_give_exact c))
+  end
+
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
     registered_e_assumption ::
@@ -174,7 +176,7 @@ and e_my_find_search db_list local_db hdc concl =
         let tac = function
         | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
         | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
-        | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl))
+        | Give_exact (c,cl) -> e_exact poly st (c,cl)
         | Res_pf_THEN_trivial_fail (term,cl) ->
           Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl)))
             (e_trivial_fail_db db_list local_db))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 1da464e6f..a1beacd5e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1097,10 +1097,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
diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v
new file mode 100644
index 000000000..ecebaba81
--- /dev/null
+++ b/test-suite/bugs/closed/4450.v
@@ -0,0 +1,58 @@
+Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop.
+
+Polymorphic Axiom unit@{u} : Type@{u}.
+Polymorphic Axiom tt@{u} : inhabited unit@{u}.
+
+Polymorphic Hint Resolve tt : the_lemmas.
+Set Printing All.
+Set Printing Universes.
+Goal inhabited unit.
+Proof.
+  eauto with the_lemmas.
+Qed.
+
+Universe u.
+Axiom f : Type@{u} -> Prop.
+Lemma fapp (X : Type) : f X -> False.
+Admitted.
+Polymorphic Axiom funi@{i} : f unit@{i}.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto using (fapp unit funi). (* The two fapp's have different universes *)
+Qed.
+
+Hint Resolve (fapp unit funi) : mylems.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto with mylems. (* Forces the two fapps at the same level *)
+Qed.
+
+Goal (forall U, f U) -> (f unit -> False) -> False /\ False.
+  eauto. (* Forces the two fapps at the same level *)
+Qed.
+
+Polymorphic Definition MyType@{i} := Type@{i}.
+Universes l m n.
+Constraint l < m.
+Polymorphic Axiom maketype@{i} : MyType@{i}.
+
+Goal MyType@{l}.
+Proof.
+  Fail solve [ eauto using maketype@{m} ].
+  eauto using maketype.
+  Undo.
+  eauto using maketype@{n}.
+Qed.
+
+Axiom foo : forall (A : Type), list A.
+Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A.
+
+Universe x y.
+Goal list Type@{x}.
+Proof.
+  eauto using (foo Type). (* Refreshes the term *)
+  Undo.
+  eauto using foo. Show Universes.
+  Undo.
+  eauto using foop. Show Proof. Show Universes.
+Qed.
\ No newline at end of file