From 9c47194eeeb77ce15dae0125ebc7df1a980d9262 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 Mar 2020 19:48:35 +0100
Subject: [PATCH] change some other hints to a more general pattern and
 typeclass instances

---
 theories/bi/embedding.v | 2 +-
 theories/bi/plainly.v   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index bbf87f95d..92bce3d7b 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -324,4 +324,4 @@ End sbi_embed.
 [class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
 search for the other premises fail. See the proof of [monPred_objectively_plain]
 for an example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances.
+Hint Extern 4 (Plain _) => notypeclasses refine (embed_plain _ _) : typeclass_instances.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index e95776174..093b731bd 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -633,4 +633,4 @@ Hint Immediate plain_persistent : typeclass_instances.
 [class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
 search for the other premises fail. See the proof of [coreP_persistent] for an
 example where it would fail with a regular [Instance].*)
-Hint Extern 4 (Persistent (_ → _)) => eapply @impl_persistent : typeclass_instances.
+Hint Extern 4 (Persistent _) => notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances.
-- 
GitLab