Commit 1da32c56 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typo.

parent 29aba696
......@@ -28,7 +28,8 @@ Section saved_anything.
Implicit Types x y : F (iProp Σ).
Implicit Types γ : gname.
Global Instance saved_prop_persistent γ x : Persistent (saved_anything_own γ x).
Global Instance saved_anything_persistent γ x :
Persistent (saved_anything_own γ x).
Proof. rewrite /saved_anything_own; apply _. Qed.
Lemma saved_anything_alloc_strong x (G : gset gname) :
Supports Markdown
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