diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index d6817d63375f38bf3a4a3a045c105ff29a9b70a7..91fe5efe52e871ac0852fad45daed0f803dfc238 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -195,8 +195,7 @@ Section proofmode_classes.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
-Hint Extern 2 (coq_tactics.of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ |={_}=> _ => iModIntro end.
+Hint Extern 2 (coq_tactics.of_envs _ ⊢ |={_}=> _) => iModIntro.
 
 (** Fancy updates that take a step. *)
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index a323455980f4634bc216b1925739b4fe645e3607..a113eb39f6684893238672e861e87701e39004a7 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1270,19 +1270,12 @@ Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
 Hint Extern 0 (of_envs _ ⊢ _) => progress iIntros.
 Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *)
 
-(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ∗ _)%I) => ...],
-but then [eauto] mysteriously fails. See bug 4762 *)
-Hint Extern 1 (of_envs _ ⊢ _) =>
-  match goal with
-  | |- _ ⊢ _ ∧ _ => iSplit
-  | |- _ ⊢ _ ∗ _ => iSplit
-  | |- _ ⊢ ▷ _ => iNext
-  | |- _ ⊢ □ _ => iClear "*"; iAlways
-  | |- _ ⊢ ∃ _, _ => iExists _
-  | |- _ ⊢ |==> _ => iModIntro
-  | |- _ ⊢ ◇ _ => iModIntro
-  end.
-Hint Extern 1 (of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.
-Hint Extern 1 (of_envs _ ⊢ _) =>
-  match goal with |- _ ⊢ (_ ∨ _)%I => iRight end.
+Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
+Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
+Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
+Hint Extern 1 (of_envs _ ⊢ □ _) => iClear "*"; iAlways.
+Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
+Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
+Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
+Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
+Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iRight.