Commit fb07db75 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typos.

Thanks to Janno.
parent f2d7678e
Pipeline #3590 passed with stage
in 10 minutes and 33 seconds
......@@ -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.
......
Markdown is supported
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