Fix CFGV contrib: handling of global hints introducing global universes.

It was wrong, the context was readded needlessly to the local evar_map context.

3 files changed, 11 insertions, 9 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 83498cabd..0c52968a7 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) gl x)) l in
+  let l = List.map (fun x -> out_term (pf_apply (prepare_hint false false) gl x)) l in
   let n =
     match n with
       | ArgArg n -> n
diff --git a/tactics/hints.ml b/tactics/hints.ml
index dbb234036..e4f28b8eb 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 env init (sigma,c) =
+let prepare_hint check poly 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
@@ -1082,15 +1082,17 @@ let prepare_hint check env init (sigma,c) =
   let c' = iter c in
     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
-      IsConstr (c', diff)
+    if poly then IsConstr (c', diff)
+    else (Global.push_context_set false diff;
+	  IsConstr (c', Univ.ContextSet.empty))
 
 let interp_hints poly =
   fun h ->
   let env = (Global.env()) in
   let sigma = Evd.from_env env in
-  let f c =
+  let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
-      prepare_hint true (Global.env()) Evd.empty (evd,c) in
+      prepare_hint true poly (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;
@@ -1103,7 +1105,7 @@ let interp_hints poly =
     | HintsReference c ->
       let gr = global_with_alias c in
 	(PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c -> (PathAny, poly, f c)
+    | HintsConstr c -> (PathAny, poly, f poly c)
   in
   let fres (pri, b, r) =
     let path, poly, gr = fi r in
@@ -1159,7 +1161,7 @@ let expand_constructor_hints env sigma lems =
 	  (fun i -> IsConstr (mkConstructU ((ind,i+1),u), 
 			      Univ.ContextSet.empty))
     | _ ->
-	[prepare_hint false env sigma (evd,lem)]) lems
+	[prepare_hint false false 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 5a4fb7709..b7b219e2e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -151,8 +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 *) -> env -> evar_map -> 
-  open_constr -> hint_term
+val prepare_hint : bool (* Check no remaining evars *) -> bool (* polymorphic *) ->
+  env -> evar_map -> open_constr -> hint_term
 
 (** [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;