diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index d79de4913..7f904a561 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,6 +16,7 @@ open Declarations open Tacmach open Clenv open Sigma.Notations +open Context.Named.Declaration (************************************************************************) (* Tacticals re-exported from the Refiner module *) @@ -69,7 +70,7 @@ let nthDecl m gl = try List.nth (pf_hyps gl) (m-1) with Failure _ -> error "No such assumption." -let nthHypId m gl = pi1 (nthDecl m gl) +let nthHypId m gl = nthDecl m gl |> get_id let nthHyp m gl = mkVar (nthHypId m gl) let lastDecl gl = nthDecl 1 gl @@ -80,7 +81,7 @@ let nLastDecls n gl = try List.firstn n (pf_hyps gl) with Failure _ -> error "Not enough hypotheses in the goal." -let nLastHypsId n gl = List.map pi1 (nLastDecls n gl) +let nLastHypsId n gl = List.map get_id (nLastDecls n gl) let nLastHyps n gl = List.map mkVar (nLastHypsId n gl) let onNthDecl m tac gl = tac (nthDecl m gl) gl @@ -98,7 +99,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac let onNLastHyps n tac = onHyps (nLastHyps n) tac let afterHyp id gl = - fst (List.split_when (fun (hyp,_,_) -> Id.equal hyp id) (pf_hyps gl)) + fst (List.split_when (Id.equal id % get_id) (pf_hyps gl)) (***************************************) (* Clause Tacticals *) @@ -552,8 +553,7 @@ module New = struct let nthHypId m gl = (** We only use [id] *) let gl = Proofview.Goal.assume gl in - let (id,_,_) = nthDecl m gl in - id + nthDecl m gl |> get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -585,7 +585,7 @@ module New = struct let afterHyp id tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps gl in - let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in + let rem, _ = List.split_when (Id.equal id % get_id) hyps in tac rem end } |