Refine fix for handling of the universe contexts of hints, depending on

their polymorphic status _and_ locality.

4 files changed, 9 insertions, 6 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0c52968a70..b6b18719c0 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -94,7 +94,7 @@ let out_term = function
   | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
 
 let prolog_tac l n gl =
-  let l = List.map (fun x -> out_term (pf_apply (prepare_hint false false) gl x)) l in
+  let l = List.map (fun x -> out_term (pf_apply (prepare_hint false (false,true)) gl x)) l in
   let n =
     match n with
       | ArgArg n -> n
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e4f28b8eb2..9faa96a806 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1052,7 +1052,7 @@ let default_prepare_hint_ident = Id.of_string "H"
 
 exception Found of constr * types
 
-let prepare_hint check poly env init (sigma,c) =
+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.
      It is actually a bit stupid to generalize over evars since the first
@@ -1083,6 +1083,7 @@ let prepare_hint check poly env init (sigma,c) =
     if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
+    else if local then IsConstr (c', diff)
     else (Global.push_context_set false diff;
 	  IsConstr (c', Univ.ContextSet.empty))
 
@@ -1092,7 +1093,7 @@ let interp_hints poly =
   let sigma = Evd.from_env env in
   let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
-      prepare_hint true poly (Global.env()) Evd.empty (evd,c) in
+      prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
     Dumpglob.add_glob (loc_of_reference r) gr;
@@ -1161,7 +1162,7 @@ let expand_constructor_hints env sigma lems =
 	  (fun i -> IsConstr (mkConstructU ((ind,i+1),u), 
 			      Univ.ContextSet.empty))
     | _ ->
-	[prepare_hint false false env sigma (evd,lem)]) lems
+	[prepare_hint false (false,true) env sigma (evd,lem)]) lems
 
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
diff --git a/tactics/hints.mli b/tactics/hints.mli
index b7b219e2e7..e25b66b27b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -151,7 +151,8 @@ val interp_hints : polymorphic -> hints_expr -> hints_entry
 
 val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
-val prepare_hint : bool (* Check no remaining evars *) -> bool (* polymorphic *) ->
+val prepare_hint : bool (* Check no remaining evars *) ->
+  (bool * bool) (* polymorphic or monomorphic, local or global *) ->
   env -> evar_map -> open_constr -> hint_term
 
 (** [make_exact_entry pri (c, ctyp)].
diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v
index 6a2f9672d3..e71ddaf71f 100644
--- a/test-suite/bugs/closed/4354.v
+++ b/test-suite/bugs/closed/4354.v
@@ -3,8 +3,9 @@ Class Lift (T : Type).
 Axiom closed_increment : forall {T} {H : Lift T}, True.
 Create HintDb core.
 Lemma closed_monotonic T (H : Lift T) : True.
+Proof.
+  Set Printing Universes.
   auto using closed_increment. Show Universes.
 Qed.
-
 (* also fails with -nois, so the content of the hint database does not matter
 *)
\ No newline at end of file