Commit ff398120 authored by Ralf Jung's avatar Ralf Jung

apply Robbert's feedback

parent 861490f0
...@@ -827,17 +827,6 @@ Proof. ...@@ -827,17 +827,6 @@ Proof.
intros. rewrite /Frame intuitionistically_if_elim affinely_elim. intros. rewrite /Frame intuitionistically_if_elim affinely_elim.
apply sep_elim_l, _. apply sep_elim_l, _.
Qed. 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. Global Instance frame_here_pure p φ Q : FromPure false Q φ Frame p ⌜φ⌝ Q True.
Proof. Proof.
......
...@@ -25,7 +25,7 @@ Section bi_modalities. ...@@ -25,7 +25,7 @@ Section bi_modalities.
Modality _ modality_affinely_mixin. Modality _ modality_affinely_mixin.
Lemma modality_intuitionistically_mixin : Lemma modality_intuitionistically_mixin :
modality_mixin (λ P : PROP, P)%I MIEnvId MIEnvIsEmpty. modality_mixin (@bi_intuitionistically PROP) MIEnvId MIEnvIsEmpty.
Proof. Proof.
split; simpl; eauto using equiv_entails_sym, intuitionistically_emp, split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
affinely_mono, persistently_mono, intuitionistically_idemp, affinely_mono, persistently_mono, intuitionistically_idemp,
......
Markdown is supported
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