Generalize fix for auto from PMP to eauto and typeclasses eauto.

1 files changed, 9 insertions, 7 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 617c491c3..a6b53d76c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -72,16 +72,14 @@ let auto_flags_of_state st =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let unify_resolve poly flags ((c : raw_hint), clenv) =
-  Proofview.Goal.nf_enter begin fun gl ->
+let connect_hint_clenv poly (c, _, ctx) clenv gl =
   (** [clenv] has been generated by a hint-making function, so the only relevant
       data in its evarmap is the set of metas. The [evar_reset_evd] function
       below just replaces the metas of sigma by those coming from the clenv. *)
   let sigma = Proofview.Goal.sigma gl in
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (** Still, we need to update the universes *)
-  let (_, _, ctx) = c in
-  let clenv =
+  let clenv, c =
     if poly then
       (** Refresh the instance of the hint *)
       let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
@@ -91,11 +89,15 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
       (** FIXME: We're being inefficient here because we substitute the whole
           evar map instead of just its metas, which are the only ones
           mentioning the old universes. *)
-      Clenv.map_clenv map clenv
+      Clenv.map_clenv map clenv, map c
     else
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-      { clenv with evd = evd ; env = Proofview.Goal.env gl }
-  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
   let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
   Clenvtac.clenv_refine false clenv
   end