stop playing tricks with uPred_holds opacitiy. We now have proper sealing.

algebra/upred.v

@@ -10,8 +10,6 @@ Record uPred (M : cmraT) : Type := IProp {
     uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
-Global Opaque uPred_holds.
-Local Transparent uPred_holds.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
 

program_logic/lifting.v

@@ -14,7 +14,6 @@ Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
-Transparent uPred_holds.
 
 Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, ■ True)))%I.
 
@@ -59,7 +58,6 @@ Proof.
 Qed.
 
 (** Derived lifting lemmas. *)
-Opaque uPred_holds.
 Import uPred.
 
 Lemma wp_lift_atomic_step {E Φ} e1

program_logic/pviewshifts.v

@@ -43,7 +43,6 @@ Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types m : iGst Λ Σ.
-Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
 Proof.
@@ -144,7 +143,6 @@ Proof.
 Qed.
 
 (** * Derived rules *)
-Opaque uPred_holds.
 Import uPred.
 Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.

program_logic/weakestpre.v

@@ -70,7 +70,6 @@ Implicit Types P : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Transparent uPred_holds.
 
 Global Instance wp_ne E e n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
@@ -218,7 +217,6 @@ Proof.
 Qed.
 
 (** * Derived rules *)
-Opaque uPred_holds.
 Import uPred.
 Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → || e @ E {{ Φ }} ⊑ || e @ E {{ Ψ }}.
 Proof. by apply wp_mask_frame_mono. Qed.