Skip to content
Snippets Groups Projects
Verified Commit cfe2139e authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Nit: Reduce asymmetry

parent 5497aa94
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/proofmode/class_instances_updates.v
+ 1
− 1
View file @ cfe2139e
...@@ -22,7 +22,7 @@ Global Instance from_pure_bupd `{!BiBUpd PROP} a P φ : ...@@ -22,7 +22,7 @@ Global Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed. Proof. rewrite /FromPure=> <-. apply bupd_intro. Qed.
Global Instance from_pure_fupd `{!BiFUpd PROP} a E P φ : Global Instance from_pure_fupd `{!BiFUpd PROP} a E P φ :
FromPure a P φ → FromPure a (|={E}=> P) φ. FromPure a P φ → FromPure a (|={E}=> P) φ.
Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed. Proof. rewrite /FromPure=> <-. apply fupd_intro. Qed.
Global Instance into_wand_bupd `{!BiBUpd PROP} p q R P Q : Global Instance into_wand_bupd `{!BiBUpd PROP} p q R P Q :
IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q). IntoWand false false R P Q → IntoWand p q (|==> R) (|==> P) (|==> Q).
......
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