From 17970986867314e43d16de8eee4227c26b066933 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 22:46:51 +0200
Subject: [PATCH] Put frames in ht_frame_step_r on consistent sides.

---
 program_logic/hoare.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index c0d87d3e0..1e978fcd7 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -118,10 +118,10 @@ Qed.
 Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
   ((R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }})
-    ⊢ {{ R1 ★ P }} e @ (E ∪ E1) {{ λ v, Φ v ★ R3 }}.
+    ⊢ {{ P ★ R1 }} e @ (E ∪ E1) {{ λ v, Φ v ★ R3 }}.
 Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
-  setoid_rewrite (comm _ _ R3).
+  setoid_rewrite (comm _ _ R3); rewrite (comm _ _ R1).
   iApply (ht_frame_step_l _ _ E2); by repeat iSplit.
 Qed.
 
-- 
GitLab