Revert "Different treatment of atomic premise in type class."

This reverts commit 2a7755fe because
it is no longer needed after Matthieu Sozeau reverted this change in
Coq 8.6. See also the discussion:

  [Coq-Club] Coq 8.6 typeclasses behavior change

at 11/16/2016 02:14 PM.

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 :=

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.