diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 14:44:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-14 13:25:55 +0200 |
| commit | 5b432bf03f623b144871181446c68479482abe32 (patch) | |
| tree | 0911f1d01043d75d84744817e64a72389ac700a4 /tactics | |
| parent | 8894e9eb35e5529966fea699014fef83e4b270bd (diff) | |
Deprecate Refiner [evar_map ref] exported functions.
Uses internal to Refiner remain.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index dc310c542..2408b8f2b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -70,11 +70,10 @@ let first_goal gls = (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) let apply_tac_list tac glls = - let (sigr,lg) = unpackage glls in - match lg with + match glls.it with | (g1::rest) -> - let gl = apply_sig_tac sigr tac g1 in - repackage sigr (gl@rest) + let pack = tac (re_sig g1 glls.sigma) in + re_sig (pack.it @ rest) pack.sigma | _ -> user_err Pp.(str "apply_tac_list") let one_step l gl = |