From 815cabab914da534341a610b46ff53522fe32cf0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2016 10:11:55 +0100
Subject: [PATCH] Revert "Different treatment of atomic premise in type class."

This reverts commit 2a7755fee187492a6bf36a89f5f3ec0b5407a637 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        | 2 +-
 program_logic/weakestpre.v | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index f399d09d3..4d9c1633c 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 699172b24..97fee1f57 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.
-- 
GitLab