monpred test: use typed turnstile notation

75411d7d · Ralf Jung · 26534645 · 75411d7d
Commit 75411d7d authored Jun 14, 2018 by Ralf Jung
--- 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 *)