From 3f992fb9ddedf5ee01042786d81aa771c047c583 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 12 Feb 2018 10:11:20 +0100
Subject: [PATCH] Remove hacks that are no longer needed.

These were needed pre-a63f256ec115ad4f6f44d077ee57d02dd2fb9eb4.
---
 theories/proofmode/class_instances.v | 14 ++------------
 theories/proofmode/classes.v         |  4 +---
 2 files changed, 3 insertions(+), 15 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 52e0daac8..53014c94b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -812,18 +812,10 @@ Global Instance elim_modal_forall {A} P P' (Φ Ψ : A → PROP) :
 Proof.
   rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
 Qed.
-(* We use this proxy type class to make sure that the instance is only
-   used when we know that Pabs is not an existential, so that this
-   instance is only triggered when a [bi_absorbingly] modality
-   actually appears, thanks to the [Hint Mode] lower in this
-   file. Otherwise, this instance is too generic and gets used in
-   irrelevant contexts. *)
-Class ElimModalAbsorbingly Pabs P Q :=
-  elim_modal_absorbingly :> ElimModal Pabs P Q Q.
 Global Instance elim_modal_absorbingly_here P Q :
-  Absorbing Q → ElimModalAbsorbingly (bi_absorbingly P) P Q.
+  Absorbing Q → ElimModal (bi_absorbingly P) P Q Q.
 Proof.
-  rewrite /ElimModalAbsorbingly /ElimModal=> H.
+  rewrite /ElimModal=> H.
   by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
@@ -1105,8 +1097,6 @@ Global Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP)
 Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.
 End bi_instances.
 
-Hint Mode ElimModalAbsorbingly + ! - - : typeclass_instances.
-
 Section sbi_instances.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 5c2efcaf6..735b754f8 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -473,7 +473,5 @@ Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
 Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
   FromModal P Q → FromModal (tc_opaque P) Q := id.
-(* Higher precedence than [elim_modal_timeless], so that [iAssert] does not
-   loop (see test [test_iAssert_modality] in proofmode.v). *)
 Instance elim_modal_tc_opaque {PROP : bi} (P P' Q Q' : PROP) :
-  ElimModal P P' Q Q' → ElimModal (tc_opaque P) P' Q Q' | 100 := id.
+  ElimModal P P' Q Q' → ElimModal (tc_opaque P) P' Q Q' := id.
-- 
GitLab