diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v index 2e7a8c7eea2ed5eb3381ac15f90b2df3ae8c5012..abff5e6423567ebf068a919dc66ab916cc921e66 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 :=