diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 9eb60d424e19050445132e9a33514716e3da887f..c7bb90344f895e3526c9a657321603e3c61e232a 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -47,7 +47,7 @@ Local Hint Extern 10 (_ ≤ _) => lia : core.
    connective.
  *)
 
-Record uPred (M : ucmraT) : Type := IProp {
+Record uPred (M : ucmraT) : Type := UPred {
   uPred_holds :> nat → M → Prop;
 
   uPred_mono n1 n2 x1 x2 :