Make uPred_holds Opaque so we do not accidentally go into the model.

iris/lifting.v

@@ -11,6 +11,7 @@ Context {Σ : iParam}.
 Implicit Types v : ival Σ.
 Implicit Types e : iexpr Σ.
 Implicit Types σ : istate Σ.
+Transparent uPred_holds.
 
 Lemma wp_lift_step E1 E2
     (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :

iris/pviewshifts.v

@@ -30,6 +30,7 @@ Section pvs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
 Implicit Types m : icmra' Σ.
+Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
 Proof.

iris/weakestpre.v

@@ -58,6 +58,7 @@ Implicit Types P : iProp Σ.
 Implicit Types Q : ival Σ → iProp Σ.
 Implicit Types v : ival Σ.
 Implicit Types e : iexpr Σ.
+Transparent uPred_holds.
 
 Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
   E1 ⊆ E2 → (∀ v r n', n' ≤ n → ✓{n'} r → Q1 v n' r → Q2 v n' r) →

modures/logic.v

@@ -11,6 +11,8 @@ 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.
 Hint Resolve uPred_0.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.