diff options
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 11 |
1 files changed, 5 insertions, 6 deletions
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 -> |