From c64b9a559cc0c137dc3f35623a9a6099b30bf331 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Feb 2016 11:10:37 +0100
Subject: [PATCH] do not forget about sealing pvs and wp

---
 program_logic/pviewshifts.v | 1 +
 program_logic/weakestpre.v  | 1 +
 2 files changed, 2 insertions(+)

diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index f2b597942..d6dee8b2f 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 213bbcbb4..0c452428a 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.
-- 
GitLab