diff --git a/iris/model.v b/iris/model.v
index 298efd34ca08a777933bb74deb94c4c111034e8b..f01f00fc5cbe08bfed768859d892c4546b6d862a 100644
--- a/iris/model.v
+++ b/iris/model.v
@@ -216,8 +216,9 @@ Definition map {Σ : iParam} {A1 A2 B1 B2 : cofeT}
 Definition result Σ : solution (F Σ).
 Proof.
   apply (solver.result _ (@map Σ)).
-  * by intros A B r n ?; rewrite /= res_map_id.
-  * by intros A1 A2 A3 B1 B2 B3 f g f' g' P r n ?; rewrite /= res_map_compose.
+  * by intros A B r n ?; rewrite /uPred_holds /= res_map_id.
+  * by intros A1 A2 A3 B1 B2 B3 f g f' g' P r n ?;
+      rewrite /= /uPred_holds /= res_map_compose.
   * by intros A1 A2 B1 B2 n f f' [??] r;
       apply upredC_map_ne, resRA_map_contractive.
 Qed.
diff --git a/modures/logic.v b/modures/logic.v
index 1dc39fd5b7badce64306721eb260b9df8f7671ee..95dff460a055d7a2e6e76da0b4b4ca337478ebe1 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -10,7 +10,7 @@ Record uPred (M : cmraT) : Type := IProp {
   uPred_weaken x1 x2 n1 n2 :
     uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
 }.
-Arguments uPred_holds {_} _ _ _.
+Arguments uPred_holds {_} _ _ _ : simpl never.
 Hint Resolve uPred_0.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
@@ -72,7 +72,8 @@ Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
     `{!CMRAMonotone f, !CMRAMonotone g} n :
   f ={n}= g → uPredC_map f ={n}= uPredC_map g.
 Proof.
-  by intros Hfg P y n' ??; rewrite /= (dist_le _ _ _ _(Hfg y)); last lia.
+  by intros Hfg P y n' ??;
+    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
 Qed.
 
 (** logical entailement *)
@@ -227,6 +228,7 @@ Implicit Types P Q : uPred M.
 Implicit Types Ps Qs : list (uPred M).
 Implicit Types A : Type.
 Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
+Arguments uPred_holds {_} !_ _ _ /.
 
 Global Instance: PreOrder (@uPred_entails M).
 Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.