diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index a369af8d7e573341cf9ddc527b6bed7cabbd131e..d2b54213a97eeb5a64c4312515d0c7780dbc13b0 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred {
 this way. *)
 Local Coercion uPred_holds : uPred >-> Funclass.
 Bind Scope bi_scope with uPred.
-Global Arguments uPred_holds {_} _%I _ _ : simpl never.
+Global Arguments uPred_holds {_} _ _ _ : simpl never.
 Add Printing Constructor uPred.
 Global Instance: Params (@uPred_holds) 3 := {}.