Commit 7a4ff479 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove some useless `%I` delimeters.

parent 4f6d4de7
......@@ -994,25 +994,25 @@ Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl
(** FromForall *)
Global Instance from_forall_forall {A} (Φ : A PROP) :
FromForall ( x, Φ x)%I Φ.
FromForall ( x, Φ x) Φ.
Proof. by rewrite /FromForall. Qed.
Global Instance from_forall_tforall {A} (Φ : tele_arg A PROP) :
FromForall (.. x, Φ x)%I Φ.
Proof. by rewrite /FromForall bi_tforall_forall. Qed.
Global Instance from_forall_pure {A} (φ : A Prop) :
@FromForall PROP A ( a : A, φ a)%I (λ a, φ a )%I.
@FromForall PROP A a : A, φ a (λ a, φ a )%I.
Proof. by rewrite /FromForall pure_forall. Qed.
Global Instance from_forall_pure_not (φ : Prop) :
@FromForall PROP φ (¬ φ⌝)%I (λ a : φ, False)%I.
@FromForall PROP φ ¬ φ⌝ (λ a : φ, False)%I.
Proof. by rewrite /FromForall pure_forall. Qed.
Global Instance from_forall_impl_pure P Q φ :
IntoPureT P φ FromForall (P Q)%I (λ _ : φ, Q)%I.
IntoPureT P φ FromForall (P Q) (λ _ : φ, Q).
Proof.
intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
Qed.
Global Instance from_forall_wand_pure P Q φ :
IntoPureT P φ TCOr (Affine P) (Absorbing Q)
FromForall (P - Q)%I (λ _ : φ, Q)%I.
FromForall (P - Q) (λ _ : φ, Q)%I.
Proof.
intros (φ'&->&?) [|]; rewrite /FromForall; apply wand_intro_r.
- rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_r.
......@@ -1027,10 +1027,10 @@ Proof.
by rewrite persistently_forall.
Qed.
Global Instance from_forall_persistently {A} P (Φ : A PROP) :
FromForall P Φ FromForall (<pers> P)%I (λ a, <pers> (Φ a))%I.
FromForall P Φ FromForall (<pers> P) (λ a, <pers> (Φ a))%I.
Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
Global Instance from_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A PROP) :
FromForall P Φ FromForall P%I (λ a, ⎡Φ a%I).
FromForall P Φ FromForall P (λ a, ⎡Φ a%I).
Proof. by rewrite /FromForall -embed_forall => <-. Qed.
(** IntoInv *)
......
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