From ecd4e7464ad7cc1131b68eb1c9146724fed15f47 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Fri, 19 Feb 2021 09:56:50 +0100
Subject: [PATCH] Enable `Typeclasses Strict Resolution` for
 dervied_connectives.v

---
 iris/bi/derived_connectives.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 0c8ac604a..2b364896e 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 {_}.
-- 
GitLab