diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index f399d09d3f23f4a506d3f88672bc890d395439af..4d9c1633cac8ca82bd2423874fbcf052e48b18f2 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -230,7 +230,7 @@ Ltac solve_atomic :=
   end.
 Hint Extern 10 (language.atomic _) => solve_atomic.
 (* For the side-condition of elim_upd_fupd_wp_atomic *)
-Hint Extern 10 (language.atomic _) => solve_atomic : atomic.
+Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 699172b24066496c1e60970f38ac16f806df1c1e..97fee1f57d03c63c27d5cc392455c1b2a0f3f120 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -310,13 +310,12 @@ Section proofmode_classes.
     ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
+  (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
+  Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
     atomic e →
     ElimModal (|={E1,E2}=> P) P
             (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
 
-(* Lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
-Hint Extern 100 (ElimModal (|={_,_}=> _) _ (WP _ @ _ {{ _ }}) _) =>
-  eapply elim_modal_fupd_wp_atomic; solve [auto with atomic] : typeclass_instances.
+Hint Extern 0 (atomic _) => assumption : typeclass_instances.