Commit acd32497 authored by Robbert Krebbers's avatar Robbert Krebbers

Stop using deprecated `iAlways` tactic.

parent ad7eeccc
......@@ -251,11 +251,11 @@ Proof.
iDestruct ("HQQ'" with "HQ") as "HQ'".
iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
- iMod (slice_delete_empty with "Hs Hb") as (P') "(Heq & Hb)"; try done.
iMod (slice_insert_empty with "Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', (Q' P')%I. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iAlways. by iSplit; iIntros "[? $]"; iApply "HQQ'".
iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
Qed.
Lemma slice_split E q f P Q1 Q2 γ b :
......
......@@ -47,7 +47,7 @@ Section proofs.
Proof.
iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
iNext; iAlways.
iIntros "!> !>".
iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
Qed.
......
......@@ -50,7 +50,7 @@ Section core.
Proof.
split.
- iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
iAlways. by iApply HP.
iIntros "!>". by iApply HP.
- iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
by iDestruct (coreP_elim with "HcQ") as "#HQ".
Qed.
......
......@@ -149,7 +149,7 @@ Section increment_client.
(* FIXME: I am only using persistent stuff, so I should be allowed
to move this to the persisten context even without the additional □. *)
iAssert ( WP incr #l {{ _, True }})%I as "#Aupd".
{ iAlways. awp_apply incr_spec. clear x.
{ iIntros "!>". awp_apply incr_spec. clear x.
iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
(* The continuation: From after the atomic triple to the postcondition of the WP *)
......
......@@ -3218,10 +3218,10 @@ Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit : core.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit : core.
Hint Extern 1 (envs_entails _ (_ - _)) => iSplit : core.
Hint Extern 1 (envs_entails _ ( _)) => iNext : core.
Hint Extern 1 (envs_entails _ ( _)) => iAlways : core.
Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways : core.
Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways : core.
Hint Extern 1 (envs_entails _ ( _)) => iAlways : core.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro : core.
Hint Extern 1 (envs_entails _ (<pers> _)) => iModIntro : core.
Hint Extern 1 (envs_entails _ (<affine> _)) => iModIntro : core.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro : core.
Hint Extern 1 (envs_entails _ ( _, _)) => iExists _ : core.
Hint Extern 1 (envs_entails _ (.. _, _)) => iExists _ : core.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro : core.
......
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