Skip to content
Snippets Groups Projects
Commit 4fe52b0b authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 6edd9b82
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
iris/bi/plainly.v
+ 1
− 1
View file @ 4fe52b0b
...@@ -134,7 +134,7 @@ Section plainly_derived. ...@@ -134,7 +134,7 @@ Section plainly_derived.
Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _). Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
Proof. intros P Q; apply plainly_mono. Qed. Proof. intros P Q; apply plainly_mono. Qed.
(* Not an instance, see the bottom of this file *) (* Not an instance; registered as [Hint Immediate] at the bottom of this file *)
Lemma plain_persistent P : Plain P → Persistent P. Lemma plain_persistent P : Plain P → Persistent P.
Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed. Proof. intros. by rewrite /Persistent -plainly_elim_persistently. Qed.
......
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