From c35476b81c7faebf5ae2980704226a089aa2bbe5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 9 Nov 2019 11:23:08 +0100
Subject: [PATCH] An additional fix for https://github.com/coq/coq/pull/10762.

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

diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 024f6410a..6db93b131 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -93,5 +93,5 @@ Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).
   iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
-  iApply (step_fupdN_wand with "Hiter"). by iApply (fupd_mask_weaken _ _ _).
+  iApply (step_fupdN_wand with "Hiter"). by iApply fupd_mask_weaken.
 Qed.
-- 
GitLab