From e0ed90f7719571785cafde1e9e9b6b8ca380a284 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 20 Mar 2017 10:49:04 +0100
Subject: [PATCH] update std++

---
 opam.pins                      | 2 +-
 theories/base_logic/lib/core.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/opam.pins b/opam.pins
index b4cfbbf51..ee2d15f4d 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 6ffa20c8f23797f81f1bb55ab27432e897de71d5
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 0ac2b4db07bdc471421c5a4c47789087b3df074c
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 8376ee688..adf16b59d 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -46,7 +46,7 @@ Section core.
   Proof.
     split.
     - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
-      iClear "∗". iAlways. by iApply HP.
+      iAlways. by iApply HP.
     - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
       iDestruct (coreP_elim with "HcQ") as "#HQ". done.
   Qed.
-- 
GitLab