From 33620b9db75aac9115877139053fe2fbc8c281d5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Feb 2018 15:07:23 +0100
Subject: [PATCH] Note that `plainly` will be removed from the BI interface.

---
 theories/bi/interface.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 9ffaa5736..f426e478e 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -92,6 +92,7 @@ Section bi_mixin.
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
 
     (* Plainly *)
+    (* Note: plainly is about to be removed from this interface *)
     bi_mixin_plainly_mono P Q : (P ⊢ Q) → bi_plainly P ⊢ bi_plainly Q;
     bi_mixin_plainly_elim_persistently P : bi_plainly P ⊢ bi_persistently P;
     bi_mixin_plainly_idemp_2 P : bi_plainly P ⊢ bi_plainly (bi_plainly P);
-- 
GitLab