diff options
| author | Pierre-Marie Pédrot | 2020-06-16 14:40:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-23 08:51:47 +0200 |
| commit | 189f4182d6e65ada8fb5856b195b52d15bebdf3a (patch) | |
| tree | e4fccf812ccf27f4d74139a55db61812ad0ce364 | |
| parent | 213999187d506394945a4d2163802b504be0c6ac (diff) | |
Use the unification result for eauto's eapply.
Instead of dropping the unification result and calling simple eapply with
the original term, we simply use the same code path as auto and typeclass
eauto, i.e. reuse the clenv for refinement.
| -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 = |