diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v index 0c8ac604a23c267ca2ace7a4b3c65f0410de5eda..2b364896edd04d24a239bd164c4d388ff7a3163c 100644 --- a/iris/bi/derived_connectives.v +++ b/iris/bi/derived_connectives.v @@ -13,6 +13,8 @@ Global Arguments bi_wand_iff {_} _%I _%I : simpl never. Global Instance: Params (@bi_wand_iff) 1 := {}. Infix "∗-∗" := bi_wand_iff : bi_scope. +#[local] Set Typeclasses Strict Resolution. + Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P. Global Arguments Persistent {_} _%I : simpl never. Global Arguments persistent {_} _%I {_}.