diff --git a/algebra/upred.v b/algebra/upred.v
index 4a31b059dbf4c0337015387ca17ca661a34b7a22..7fd9b5bffb4bfa0fc51023a11ce18d6aafec6c8d 100644
--- a/algebra/upred.v
+++ b/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.
 
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 365716b3fa8c5437e340045b1848d182c29406e6..0982d52426db88a1f8517e58f8c68881e35736d5 100644
--- a/program_logic/lifting.v
+++ b/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
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 1268b97409c2e7779e90b83d5d7ca33fc684e83c..c606062fa8ee15a1d876d5b77d24b34921c61c56 100644
--- a/program_logic/pviewshifts.v
+++ b/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.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index fea680774a7df7532c9f8053a5d571741022158f..9a0d672335b5225973d5fc0e3b0c02b707a69d1c 100644
--- a/program_logic/weakestpre.v
+++ b/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.