From fb07db75474fbfae3c390cba2663ee6ac78f1ce2 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 5 Jan 2017 11:59:09 +0100 Subject: [PATCH] Fix typos. Thanks to Janno. --- theories/base_logic/lib/sts.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v index a87844443..8776ec6c4 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. -- GitLab