From 82942fc055f58c8e12a85663208829e9514235fd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 4 Jun 2019 00:05:24 +0200
Subject: [PATCH] Remove some useless parentheses.

---
 theories/heap_lang/lifting.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index dd20b4cef..18f992536 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -253,8 +253,8 @@ Qed.
 (** Heap *)
 Lemma wp_allocN s E v n :
   0 < n →
-  {{{ True }}} AllocN ((Val $ LitV $ LitInt $ n)) (Val v) @ s; E
-  {{{ l, RET LitV (LitLoc l); l ↦∗ (replicate (Z.to_nat n) v) }}}.
+  {{{ True }}} AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
+  {{{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }}}.
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
@@ -268,8 +268,8 @@ Proof.
 Qed.
 Lemma twp_allocN s E v n :
   0 < n →
-  [[{ True }]] AllocN ((Val $ LitV $ LitInt $ n)) (Val v) @ s; E
-  [[{ l, RET LitV (LitLoc l); l ↦∗ (replicate (Z.to_nat n) v) }]].
+  [[{ True }]] AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E
+  [[{ l, RET LitV (LitLoc l); l ↦∗ replicate (Z.to_nat n) v }]].
 Proof.
   iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
-- 
GitLab