From 5b432bf03f623b144871181446c68479482abe32 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:44:30 +0200
Subject: Deprecate Refiner [evar_map ref] exported functions.

Uses internal to Refiner remain.
---
 tactics/eauto.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'tactics')

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 =
-- 
cgit v1.2.3