diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
| commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
| tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /tactics/eauto.ml | |
| parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) | |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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 -> |