From 8bb5541f94c0d38ce04f01262637163fe02fc5f3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Oct 2018 08:57:48 +0200
Subject: [PATCH] whitespace tweaks

---
 theories/heap_lang/lang.v      | 15 ++++++++++++---
 theories/heap_lang/proofmode.v |  1 -
 2 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 9242baac2..3bccac51b 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -477,7 +477,10 @@ Inductive head_step : expr → state → option observation -> expr → state 
      head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ.1 !! l) →
-     head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ.1, σ.2) []
+     head_step (Store (Lit $ LitLoc l) e) σ
+               None
+               (Lit LitUnit) (<[l:=v]>σ.1, σ.2)
+               []
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ.1 !! l = Some vl → vl ≠ v1 →
@@ -487,11 +490,17 @@ Inductive head_step : expr → state → option observation -> expr → state 
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ.1 !! l = Some v1 →
      vals_cas_compare_safe v1 v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2) []
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ
+               None
+               (Lit $ LitBool true) (<[l:=v2]>σ.1, σ.2)
+               []
   | FaaS l i1 e2 i2 σ :
      to_val e2 = Some (LitV (LitInt i2)) →
      σ.1 !! l = Some (LitV (LitInt i1)) →
-     head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ.1, σ.2) []
+     head_step (FAA (Lit $ LitLoc l) e2) σ
+               None
+               (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ.1, σ.2)
+               []
   | NewProphS σ p :
      p ∉ σ.2 →
      head_step NewProph σ None (Lit $ LitProphecy p) (σ.1, {[ p ]} ∪ σ.2) []
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index de11f87f6..e2324fd40 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -40,7 +40,6 @@ Proof.
   rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -lifting.wp_pure_step_later //.
 Qed.
-
 Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-- 
GitLab