diff --git a/opam b/opam index 4a40ed1055dd5a3e0e72033e1643e03ecbe3cd4d..34f8970f23d4b97cfd34e831d07392ab036a7f71 100644 --- a/opam +++ b/opam @@ -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-06.2.f5d03e25") | (= "dev") } + "coq-iris" { (= "dev.2019-03-14.2.66a69b0a") | (= "dev") } ] diff --git a/theories/c_translation/proofmode.v b/theories/c_translation/proofmode.v index b559ceba730565fc7377d2b77664bfac8c3f05f9..19842c2ebb326faa3f6d054feb7d3781126d15c3 100644 --- a/theories/c_translation/proofmode.v +++ b/theories/c_translation/proofmode.v @@ -78,7 +78,7 @@ Ltac cwp_pures := Tactic Notation "cwp_rec" := let H := fresh in - assert (H := AsRecV_recv_locked); + assert (H := AsRecV_recv); cwp_pure (App _ _); clear H. diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index 937fe6ccf1ff50ccaef950a966cbfb5e2b682a59..17cd6346aa499d9e86cbba485447784fc4cca98a 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -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 -lock. cwp_pures. + iIntros "H". rewrite /c_if. 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 -lock. cwp_pures. + iIntros "H". cwp_lam. cwp_pures. rewrite /c_if. 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]] !> !>".