diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v index a87844443106f691ee8f1f71b00b5355d099ac78..8776ec6c4b9588e205522c6227616af9a3f9bcf3 100644 --- a/theories/base_logic/lib/sts.v +++ b/theories/base_logic/lib/sts.v @@ -45,9 +45,9 @@ Section definitions. Proof. solve_proper. Qed. Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ). Proof. apply _. Qed. - Global Instance sts_own_peristent s : PersistentP (sts_own s ∅). + Global Instance sts_own_persistent s : PersistentP (sts_own s ∅). Proof. apply _. Qed. - Global Instance sts_ownS_peristent S : PersistentP (sts_ownS S ∅). + Global Instance sts_ownS_persistent S : PersistentP (sts_ownS S ∅). Proof. apply _. Qed. End definitions.