From 9e33557cc00c27e1c6532b56f5fb8545b5e1d40b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Dec 2017 18:29:23 +0100
Subject: [PATCH] Use `iEval ... in ...` somewhere.

---
 theories/base_logic/lib/boxes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index cf8aff8a0..52e4d2bd1 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -209,7 +209,7 @@ Lemma box_fill E f P :
 Proof.
   iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR; first by rewrite big_opM_fmap.
-  rewrite internal_eq_iff later_iff big_opM_commute.
+  iEval (rewrite internal_eq_iff later_iff big_opM_commute) in "HeqP".
   iDestruct ("HeqP" with "HP") as "HP".
   iCombine "Hf" "HP" as "Hf".
   rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
-- 
GitLab