diff options
| author | Matthieu Sozeau | 2020-06-24 15:10:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-06-24 15:10:56 +0200 |
| commit | 0465e99e6fa993064a4a630c873ed25225e2c876 (patch) | |
| tree | e7eeae5b79b72b0297832898d39c83af8eb8d268 /tactics | |
| parent | 3ba88c944db09003caaa668699230613b1bca793 (diff) | |
| parent | c1f70486cd62cbd65176c8799077b48dd2c93797 (diff) | |
Merge PR #12532: Use the unification result for eauto's eapply.
Reviewed-by: mattam82
Diffstat (limited to 'tactics')
| -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 = |