diff options
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 686303a2ab..9a554b117e 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -19,7 +19,6 @@ open Tacticals open Tacmach open Evd open Tactics -open Clenv open Auto open Genredexpr open Tactypes @@ -66,10 +65,7 @@ open Auto (***************************************************************************) let unify_e_resolve flags h = - Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv' - end + Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h let hintmap_of sigma secvars concl = (* Warning: for computation sharing, we need to return a closure *) @@ -87,10 +83,10 @@ let hintmap_of sigma secvars concl = let e_exact flags h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv h gl in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (e_give_exact c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, c = Hints.fresh_hint env sigma h in + Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c end let rec e_trivial_fail_db db_list local_db = |