Commit 419e96d8 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make unseal collections `Local`.

parent 088999ea
......@@ -426,7 +426,7 @@ Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
These are not directly usable later because they do not refer to the BI
connectives. *)
Module uPred_primitive.
Definition uPred_unseal :=
Local Definition uPred_unseal :=
(uPred_pure_unseal, uPred_and_unseal, uPred_or_unseal, uPred_impl_unseal,
uPred_forall_unseal, uPred_exist_unseal, uPred_internal_eq_unseal,
uPred_sep_unseal, uPred_wand_unseal, uPred_plainly_unseal,
......
......@@ -255,7 +255,7 @@ Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
Module MonPred.
Definition monPred_unseal :=
Local Definition monPred_unseal :=
(@monPred_and_unseal, @monPred_or_unseal, @monPred_impl_unseal,
@monPred_forall_unseal, @monPred_exist_unseal, @monPred_sep_unseal,
@monPred_wand_unseal, @monPred_persistently_unseal, @monPred_later_unseal,
......
......@@ -123,7 +123,7 @@ Local Definition siProp_later_unseal :
These are not directly usable later because they do not refer to the BI
connectives. *)
Module siProp_primitive.
Definition siProp_unseal :=
Local Definition siProp_unseal :=
(siProp_pure_unseal, siProp_and_unseal, siProp_or_unseal,
siProp_impl_unseal, siProp_forall_unseal, siProp_exist_unseal,
siProp_internal_eq_unseal, siProp_later_unseal).
......
Supports Markdown
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