Commit 3f992fb9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove hacks that are no longer needed.

These were needed pre-a63f256e.
parent 7e816a90
......@@ -812,18 +812,10 @@ Global Instance elim_modal_forall {A} P P' (Φ Ψ : A → PROP) :
rewrite /ElimModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
(* 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.
rewrite /ElimModalAbsorbingly /ElimModal=> H.
rewrite /ElimModal=> H.
by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
......@@ -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.
......@@ -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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment