From 9e5b4d6a066c7701ac4107b58348e8843a5f8d18 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 9 Dec 2016 09:02:59 +0100
Subject: [PATCH] fix compilation with Coq 8.5

---
 theories/lang/derived.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index 3e5b3794..0f4519c0 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -56,7 +56,7 @@ Qed.
 
 Lemma wp_offset E l z Φ :
   ▷ (|={E}=> Φ (LitV $ LitLoc $ shift_loc l z)) -∗
-    WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $LitInt z) @ E {{ Φ }}.
+    WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.
 Proof.
   iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
   iNext. iIntros (?? Heval). inversion_clear Heval. done.
@@ -64,7 +64,7 @@ Qed.
 
 Lemma wp_plus E z1 z2 Φ :
   ▷ (|={E}=> Φ (LitV $ LitInt $ z1 + z2)) -∗
-    WP BinOp PlusOp (Lit $ LitInt z1) (Lit $LitInt z2) @ E {{ Φ }}.
+    WP BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
 Proof.
   iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
   iNext. iIntros (?? Heval). inversion_clear Heval. done.
@@ -72,7 +72,7 @@ Qed.
 
 Lemma wp_minus E z1 z2 Φ :
   ▷ (|={E}=> Φ (LitV $ LitInt $ z1 - z2)) -∗
-    WP BinOp MinusOp (Lit $ LitInt z1) (Lit $LitInt z2) @ E {{ Φ }}.
+    WP BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2) @ E {{ Φ }}.
 Proof.
   iIntros "HP". iApply wp_fupd. iApply wp_bin_op_pure; first by econstructor.
   iNext. iIntros (?? Heval). inversion_clear Heval. done.
-- 
GitLab