Fix Hint Modes and add some.

theories/bi/embedding.v

@@ -38,6 +38,7 @@ Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
   embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤;
   embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢ (P ≡ Q : PROP');
 }.
+Hint Mode BiEmbed + + ! ! : typeclass_instances.
 
 Section embed_laws.
   Context `{BiEmbed PROP1 PROP2}.

theories/bi/updates.v

@@ -82,14 +82,16 @@ Class BiFUpd (PROP : sbi) := {
   bi_fupd_fupd :> FUpd PROP;
   bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
 }.
-Hint Mode BiBUpd ! : typeclass_instances.
+Hint Mode BiFUpd ! : typeclass_instances.
 Arguments bi_fupd_fupd : simpl never.
 
 Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
   bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
+Hint Mode BiBUpdFUpd + ! ! : typeclass_instances.
 
 Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
   bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
+Hint Mode BiBUpdPlainly + ! ! : typeclass_instances.
 
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
@@ -98,6 +100,7 @@ Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   later_fupd_plain E (P : PROP) `{!Plain P} :
     (▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
 }.
+Hint Mode BiBUpdFUpd + ! ! : typeclass_instances.
 
 Section bupd_laws.
   Context `{BiBUpd PROP}.