Commit 0c4025c2 authored by Ralf Jung's avatar Ralf Jung

Revert "Bump Iris."

This reverts commit b1eb1a06, to get initial timing without that commit.
parent b1eb1a06
Pipeline #15466 canceled with stage
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-03-14.2.66a69b0a") | (= "dev") }
"coq-iris" { (= "dev.2019-03-06.2.f5d03e25") | (= "dev") }
]
......@@ -78,7 +78,7 @@ Ltac cwp_pures :=
Tactic Notation "cwp_rec" :=
let H := fresh in
assert (H := AsRecV_recv);
assert (H := AsRecV_recv_locked);
cwp_pure (App _ _);
clear H.
......
......@@ -483,7 +483,7 @@ Section proofs.
(v = #false U (CWP e2 @ R {{ Φ }})) }} -
CWP if (c) { e1 } else { e2 } @ R {{ Φ }}.
Proof.
iIntros "H". rewrite /c_if. cwp_pures.
iIntros "H". rewrite /c_if -lock. cwp_pures.
cwp_apply (cwp_wp with "H"). iIntros (v) "H". cwp_pures.
iApply cwp_seq_bind'. iApply (cwp_wand with "H").
iIntros (v') "[[-> ?] | [-> ?]] !> !>"; by cwp_pures.
......@@ -501,7 +501,7 @@ Section proofs.
v = #false U (Φ #()) }} -
CWP whileV (c) { e } @ R {{ Φ }}.
Proof.
iIntros "H". cwp_lam. cwp_pures. rewrite /c_if. cwp_pures.
iIntros "H". cwp_lam. cwp_pures. rewrite /c_if -lock. cwp_pures.
cwp_apply (cwp_wp with "H"). iIntros (v) "H". cwp_lam. cwp_pures.
iApply cwp_seq_bind'. iApply (cwp_wand with "H").
iIntros (v') "[[-> H] | [-> H]] !> !>".
......
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