From 5f3931102053c5001a67d3f79f17add534d5b694 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 10 Feb 2016 10:58:51 +0100
Subject: [PATCH] make some nested function calls in heap_lang/ more readable

---
 heap_lang/heap_lang.v | 10 +++++-----
 heap_lang/lifting.v   |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index a77b36995..6f0fee142 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -165,11 +165,11 @@ Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
 
 Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   match op, l1, l2 with
-  | PlusOp, LitNat n1, LitNat n2 => Some (LitNat (n1 + n2))
-  | MinusOp, LitNat n1, LitNat n2 => Some (LitNat (n1 - n2))
-  | LeOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 ≤ n2)))
-  | LtOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 < n2)))
-  | EqOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 = n2)))
+  | PlusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 + n2)
+  | MinusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 - n2)
+  | LeOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 ≤ n2)
+  | LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 < n2)
+  | EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 = n2)
   | _, _, _ => None
   end.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index b68d8ea3b..ffd501bf3 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -130,7 +130,7 @@ Qed.
 
 Lemma wp_fst E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
+  ▷ Q v1 ⊑ wp E (Fst $ Pair e1 e2) Q.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
     last by intros; inv_step; eauto.
@@ -139,7 +139,7 @@ Qed.
 
 Lemma wp_snd E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
-  ▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
+  ▷ Q v2 ⊑ wp E (Snd $ Pair e1 e2) Q.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
     last by intros; inv_step; eauto.
-- 
GitLab