From 23c54a2718234aba94ffe06be65d29b01a1cf87f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Feb 2016 19:13:13 +0100
Subject: [PATCH] heap_lang: get rid of some unnecessary parenthesis

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

diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 572d95cc3..8c0058204 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -53,9 +53,9 @@ Module LiftingTests.
   Qed.
 
   Definition FindPred (n2 : expr) : expr :=
-    rec:: (let: #1 + Lit 1 in if #0 < n2.[ren(+3)] then #1 #0 else #2).
+    rec:: let: #1 + Lit 1 in if #0 < n2.[ren(+3)] then #1 #0 else #2.
   Definition Pred : expr :=
-    λ: (if #0 ≤ Lit 0 then Lit 0 else FindPred #0 (Lit 0))%L.
+    λ: if #0 ≤ Lit 0 then Lit 0 else FindPred #0 (Lit 0).
 
   Lemma FindPred_spec n1 n2 E Q :
     (■ (n1 < n2) ∧ Q (LitV $ pred n2)) ⊑ wp E (FindPred (Lit n2) (Lit n1)) Q.
-- 
GitLab