From f28788965f756913d457bf6fac399f6f8c60baca Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jun 2018 23:25:51 +0200
Subject: [PATCH] Plain typeclass should not require BiPlainly instance to be
 inferred

---
 theories/bi/plainly.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 2e7a8c7ee..abff5e642 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -86,7 +86,7 @@ End plainly_laws.
 Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
 Arguments Plain {_ _} _%I : simpl never.
 Arguments plain {_ _} _%I {_}.
-Hint Mode Plain + ! ! : typeclass_instances.
+Hint Mode Plain + - ! : typeclass_instances.
 Instance: Params (@Plain) 1.
 
 Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
-- 
GitLab