From b5ad0e0f3af02358b904b6a951c8c29dbff7933c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Apr 2016 12:58:50 +0200
Subject: [PATCH] minor formatting nits

---
 heap_lang/lib/lock.v    | 6 +++---
 proofmode/coq_tactics.v | 4 ++--
 tests/heap_lang.v       | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 511d3a87e..a74e0ad5f 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -52,12 +52,12 @@ Lemma newlock_spec N (R : iProp) Φ :
   (heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ (LocV l)))
   ⊢ WP newlock #() {{ Φ }}.
 Proof.
-  iIntros {?} "(#Hh&HR&HΦ)". rewrite /newlock.
+  iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
   wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (lock_inv γ l R)) "[HR Hl Hγ]" as "#?"; first done.
+  iPvs (inv_alloc N _ (lock_inv γ l R)) "-[HΦ]" as "#?"; first done.
   { iNext. iExists false. by iFrame "Hl HR". }
-  iPvsIntro; iApply "HΦ". iExists N, γ. by repeat iSplit.
+  iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
 Qed.
 
 Lemma acquire_spec l R (Φ : val → iProp) :
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index a897a0827..3502c54ba 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -570,7 +570,7 @@ Qed.
 (** * Rewriting *)
 Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
   envs_lookup i Δ = Some (p, Pxy) →
-  ∀ {A : cofeT} x y (Φ : A → uPred M),
+  ∀ {A : cofeT} (x y : A) (Φ : A → uPred M),
     Pxy ⊢ (x ≡ y)%I →
     Q ⊣⊢ Φ (if lr then y else x) →
     (∀ n, Proper (dist n ==> dist n) Φ) →
@@ -761,7 +761,7 @@ Global Instance or_destruct_later P Q1 Q2 :
 Proof. rewrite /OrDestruct=>->. by rewrite later_or. Qed.
 
 Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
-  envs_lookup i Δ = Some (p, P)%I → OrDestruct P P1 P2 →
+  envs_lookup i Δ = Some (p, P) → OrDestruct P P1 P2 →
   envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
   envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
   Δ1 ⊢ Q → Δ2 ⊢ Q → Δ ⊢ Q.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f10a57d99..853b38f42 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -70,6 +70,6 @@ Section ClosedProofs.
   Proof.
     iProof. iIntros "! Hσ".
     iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
-    iApply heap_e_spec; last done ; by rewrite nclose_nroot.
+    iApply heap_e_spec; last done; by rewrite nclose_nroot.
   Qed.
 End ClosedProofs.
-- 
GitLab