Commit 962637df authored by Ralf Jung's avatar Ralf Jung

avoid deprecated !#

parent 226ad3bc
...@@ -29,7 +29,7 @@ Section basic_tests. ...@@ -29,7 +29,7 @@ Section basic_tests.
Proof. iIntros (H) "!%". done. Qed. Proof. iIntros (H) "!%". done. Qed.
Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT PROP) : Lemma test_pure_tforall_persistent {TT : tele} (Φ : TT PROP) :
(.. x, <pers> (Φ x)) - <pers> .. x, Φ x. (.. x, <pers> (Φ x)) - <pers> .. x, Φ x.
Proof. iIntros "#H !#" (x). done. Qed. Proof. iIntros "#H !>" (x). done. Qed.
Lemma test_pure_texists_intuitionistic {TT : tele} (Φ : TT PROP) : Lemma test_pure_texists_intuitionistic {TT : tele} (Φ : TT PROP) :
(.. x, (Φ x)) - .. x, Φ x. (.. x, (Φ x)) - .. x, Φ x.
Proof. iDestruct 1 as (x) "#H". iExists (x). done. Qed. Proof. iDestruct 1 as (x) "#H". iExists (x). done. Qed.
......
...@@ -60,7 +60,7 @@ Section instances. ...@@ -60,7 +60,7 @@ Section instances.
Proof. Proof.
rewrite /Laterable. iIntros (LΦ). iDestruct 1 as (x) "H". rewrite /Laterable. iIntros (LΦ). iDestruct 1 as (x) "H".
iDestruct (LΦ with "H") as (Q) "[HQ #HΦ]". iDestruct (LΦ with "H") as (Q) "[HQ #HΦ]".
iExists Q. iIntros "{$HQ} !# HQ". iExists x. by iApply "HΦ". iExists Q. iIntros "{$HQ} !> HQ". iExists x. by iApply "HΦ".
Qed. Qed.
Global Instance big_sepL_laterable Ps : Global Instance big_sepL_laterable Ps :
......
...@@ -51,7 +51,7 @@ Section proof. ...@@ -51,7 +51,7 @@ Section proof.
Proof. Proof.
iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR". iDestruct 1 as (l ->) "#Hinv"; iIntros "#HR".
iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv"). iExists l; iSplit; [done|]. iApply (inv_iff with "Hinv").
iIntros "!> !#"; iSplit; iDestruct 1 as (b) "[Hl H]"; iIntros "!> !>"; iSplit; iDestruct 1 as (b) "[Hl H]";
iExists b; iFrame "Hl"; destruct b; iExists b; iFrame "Hl"; destruct b;
first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"]. first [done|iDestruct "H" as "[$ ?]"; by iApply "HR"].
Qed. Qed.
......
...@@ -75,7 +75,7 @@ Section proof. ...@@ -75,7 +75,7 @@ Section proof.
Proof. Proof.
iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR". iDestruct 1 as (lo ln ->) "#Hinv"; iIntros "#HR".
iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv"). iExists lo, ln; iSplit; [done|]. iApply (inv_iff with "Hinv").
iIntros "!> !#"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)"; iIntros "!> !>"; iSplit; iDestruct 1 as (o n) "(Ho & Hn & H● & H)";
iExists o, n; iFrame "Ho Hn H●"; iExists o, n; iFrame "Ho Hn H●";
(iDestruct "H" as "[[H◯ H]|H◯]"; [iLeft; iFrame "H◯"; by iApply "HR"|by iRight]). (iDestruct "H" as "[[H◯ H]|H◯]"; [iLeft; iFrame "H◯"; by iApply "HR"|by iRight]).
Qed. Qed.
......
...@@ -229,7 +229,7 @@ Lemma wp_rec_löb s E f x e Φ Ψ : ...@@ -229,7 +229,7 @@ Lemma wp_rec_löb s E f x e Φ Ψ :
Proof. Proof.
iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ". iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
iApply lifting.wp_pure_step_later; first done. iApply lifting.wp_pure_step_later; first done.
iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!#" (w) "HΨ". iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
iApply ("IH" with "HΨ"). iApply ("IH" with "HΨ").
Qed. Qed.
......
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