From 1da32c56d8b176b223d95138c5e7ec7995358490 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 15 Nov 2017 17:15:15 +0100 Subject: [PATCH] Fix typo. --- theories/base_logic/lib/saved_prop.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v index 54c72a4ce..8d9939d90 100644 --- a/theories/base_logic/lib/saved_prop.v +++ b/theories/base_logic/lib/saved_prop.v @@ -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) : -- GitLab