From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 tactics/eauto.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dc310c54..80d07c5c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Term
+open Constr
 open Termops
 open EConstr
 open Proof_type
@@ -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 =
@@ -90,7 +89,7 @@ let rec prolog l n gl =
 
 let out_term env = function
   | IsConstr (c, _) -> c
-  | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr))
+  | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr))
 
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
-- 
cgit v1.2.3