Skip to content

GitLab

Commit 254e94b2 authored by Simon Hudon's avatar Simon Hudon
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 350f5ecf
Hide whitespace changes
Inline Side-by-side
iris_heap_lang/proofmode.v
View file @ 254e94b2
...@@ -385,7 +385,7 @@ Proof. ...@@ -385,7 +385,7 @@ Proof.
rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg. rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl. rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. rewrite right_id.
by apply later_mono, sep_mono_r, wand_mono. by apply later_mono, sep_mono_r, wand_mono.
Qed. Qed.
Lemma tac_twp_xchg Δ s E i K l v v' Φ : Lemma tac_twp_xchg Δ s E i K l v v' Φ :
envs_lookup i Δ = Some (false, l ↦ v)%I → envs_lookup i Δ = Some (false, l ↦ v)%I →
......
Supports Markdown
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