From 75411d7d2b6484e1be33f54a37c50a781f1fca91 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jun 2018 11:04:43 +0200
Subject: [PATCH] monpred test: use typed turnstile notation

---
 tests/proofmode_monpred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 958d37062..c683a11a7 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -121,7 +121,7 @@ Section tests.
   Qed.
 
   Lemma test_iNext_Bi P :
-    @bi_entails monPredI (â–· P) (â–· P).
+    ▷ P ⊢@{monPredI} ▷ P.
   Proof. iIntros "H". by iNext. Qed.
 
   (** Test monPred_at framing *)
-- 
GitLab