diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index f2b597942774fdfa33346f2d12f6affe3bafbd2f..d6dee8b2fdb009984a89cc684c467037b723f083 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -9,6 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
   | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
   end; solve_validN.
 
+(* TODO: Consider sealing this, like all the definitions in upred.v. *)
 Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
   {| uPred_holds n r1 := ∀ rf k Ef σ,
        0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ →
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 213bbcbb4b41592d8d6195d42380db9e829a9089..0c452428a5aaf8e907a5fe931d42c14ea039c40f 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -30,6 +30,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset)
        wp_go (E ∪ Ef) (wp_pre E Φ)
                       (wp_pre ⊤ (λ _, True%I)) k rf e1 σ1) →
      wp_pre E Φ e1 n r1.
+(* TODO: Consider sealing this, like all the definitions in upred.v. *)
 Program Definition wp {Λ Σ} (E : coPset) (e : expr Λ)
   (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ := {| uPred_holds := wp_pre E Φ e |}.
 Next Obligation.