diff options
| -rw-r--r-- | tactics/eauto.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 0ff90bc046..90e4aaa167 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -69,9 +69,7 @@ let unify_e_resolve flags h = Proofview.Goal.enter begin fun gl -> let clenv', c = connect_hint_clenv h gl in let clenv' = clenv_unique_resolver ~flags clenv' gl in - Proofview.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (Tactics.Simple.eapply c) + Clenvtac.clenv_refine ~with_evars:true ~with_classes:true clenv' end let hintmap_of sigma secvars concl = |