Commit 4c08cbe9 authored by Dan Frumin's avatar Dan Frumin

Small optimization in rel_apply

rel_apply_ tactic pose the lemma before searching for a place to apply
it.
This is in accordance with <https://gitlab.mpi-sws.org/FP/iris-coq/commit/211dc7cad10da872d2840f73acd85eed0b82f7b4>
parent 21f897d7
......@@ -42,16 +42,24 @@ Tactic Notation "rel_vals" :=
Tactic Notation "rel_apply_l" open_constr(lem) :=
iStartProof;
rel_reshape_cont_l ltac:(fun K e =>
rel_bind_ctx_l K; iApply lem; tac_rel_done; try iNext; simpl_subst/=)
|| fail "rel_apply_l: Cannot apply " lem.
(iPoseProofCore lem as false true (fun H =>
rel_reshape_cont_l ltac:(fun K e =>
rel_bind_ctx_l K;
iApplyHyp H;
try iNext; simpl_subst/=)
|| lazymatch iTypeOf H with
| Some (_,?P) => fail "rel_apply_l: Cannot apply" P
end)); tac_rel_done.
Tactic Notation "rel_apply_r" open_constr(lem) :=
iStartProof;
rel_reshape_cont_r ltac:(fun K e =>
rel_bind_ctx_r K; iApply lem; tac_rel_done; try iNext; simpl_subst/=)
|| fail "rel_apply_r: Cannot apply " lem.
(iPoseProofCore lem as false true (fun H =>
rel_reshape_cont_r ltac:(fun K e =>
rel_bind_ctx_r K;
iApplyHyp H;
try iNext; simpl_subst/=)
|| lazymatch iTypeOf H with
| Some (_,?P) => fail "rel_apply_r: Cannot apply" P
end)); tac_rel_done.
(** Pure reductions *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment