From 2f61a6b77a035b9be500f8d1707b89aafabfaf81 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 22 Jan 2017 11:26:48 +0100
Subject: [PATCH] Use uPred_pure for instead of uPred_forall in core.v.

---
 theories/base_logic/lib/core.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 6630d803a..d070516b9 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -8,7 +8,7 @@ Import uPred.
     in the shallow embedding. *)
 
 Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
-  (∀ `(!PersistentP Q, P ⊢ Q), Q)%I.
+  (∀ `(!PersistentP Q), ⌜P ⊢ Q⌝ → Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -25,7 +25,7 @@ Section core.
   Global Instance coreP_mono : Proper ((⊢) ==> (⊢)) (@coreP M).
   Proof.
     rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??).
-    unshelve iApply ("H" $! Q). by etrans.
+    iApply ("H" $! Q with "[%]"). by etrans.
   Qed.
 
   Global Instance coreP_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@coreP M).
-- 
GitLab