Commit 9aa9b311 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 0a81f4ef 121a4a75
......@@ -376,6 +376,11 @@ Proof.
eapply closed_steps, Hsup; first done. set_solver +Hs'.
Qed.
Global Instance sts_frag_peristent S : Persistent (sts_frag S ).
Proof.
constructor; split=> //= [[??]]. by rewrite /dra.dra_core /= sts.up_closed.
Qed.
(** Inclusion *)
(* This is surprisingly different from to_validity_included. I am not sure
whether this is because to_validity_included is non-canonical, or this
......
......@@ -44,6 +44,10 @@ Section definitions.
Proof. solve_proper. Qed.
Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
Proof. apply _. Qed.
Global Instance sts_own_peristent s : PersistentP (sts_own s ).
Proof. apply _. Qed.
Global Instance sts_ownS_peristent S : PersistentP (sts_ownS S ).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
......
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