diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index 04a7712dcb7ac83c2921b055eee6c454946b3927..749685bb20297e011844ded7cb923cc27afb6d00 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 bde99d57480db8b42c97048f19f73ea514c415ca..e58f0e8cebe2d0eade40270a8a6e8d21ef574843 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 70e0ba8ab51323c7317d357eae328f62e7b77ec3..8a6b499b0da8d27836225d94d3f4ebee6d21b78b 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).