From 419e96d894df9bc8a4eadbb47d43d7a6c3b60d54 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 May 2022 09:58:46 +0200
Subject: [PATCH] Make unseal collections `Local`.
---
iris/base_logic/upred.v | 2 +-
iris/bi/monpred.v | 2 +-
iris/si_logic/siprop.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 04a7712dc..749685bb2 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -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,
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index bde99d574..e58f0e8ce 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -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,
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 70e0ba8ab..8a6b499b0 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -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).
--
GitLab