diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v index 54c72a4ce45ac8cac5d933587f835402072b1956..8d9939d90593e5070c1bfff3a5a55becec1251dc 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) :