From ff3981203c8626a387b224857543a37ef03d5cdc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Mar 2018 09:15:30 +0100
Subject: [PATCH] apply Robbert's feedback

---
 theories/proofmode/class_instances.v    | 11 -----------
 theories/proofmode/modality_instances.v |  2 +-
 2 files changed, 1 insertion(+), 12 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c01ce3b53..58f729c7f 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -827,17 +827,6 @@ Proof.
   intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
   apply sep_elim_l, _.
 Qed.
-Global Instance frame_intuitionistically_here_absorbing p R :
-  Absorbing R → Frame p (□ R) R True | 0.
-Proof.
-  intros. rewrite /Frame intuitionistically_if_elim intuitionistically_elim.
-  apply sep_elim_l, _.
-Qed.
-Global Instance frame_intuitionistically_here p R : Frame p (â–¡ R) R emp | 1.
-Proof.
-  intros. rewrite /Frame intuitionistically_if_elim intuitionistically_elim.
-  apply sep_elim_l, _.
-Qed.
 
 Global Instance frame_here_pure p φ Q : FromPure false Q φ → Frame p ⌜φ⌝ Q True.
 Proof.
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index b780300aa..6018b7aae 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -25,7 +25,7 @@ Section bi_modalities.
     Modality _ modality_affinely_mixin.
 
   Lemma modality_intuitionistically_mixin :
-    modality_mixin (λ P : PROP, □ P)%I MIEnvId MIEnvIsEmpty.
+    modality_mixin (@bi_intuitionistically PROP) MIEnvId MIEnvIsEmpty.
   Proof.
     split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
       affinely_mono, persistently_mono, intuitionistically_idemp,
-- 
GitLab