From e31f803429920465a87981b864b71cf6f240afa4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Feb 2018 13:14:26 +0100
Subject: [PATCH] avoid type ascription

---
 theories/bi/updates.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 07c9185c8..ab8117037 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -133,7 +133,7 @@ Section fupd_derived.
 
   Lemma fupd_intro E P : P ={E}=∗ P.
   Proof. rewrite -bupd_fupd. apply bupd_intro. Qed.
-  Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> emp : PROP)%I.
+  Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
   Proof. exact: fupd_intro_mask. Qed.
   Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
   Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
-- 
GitLab