diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index 1b7fbda601..b1aecf6eef 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -964,7 +964,7 @@ Qed.
 
 (** ** Treeify *)
 
-Abbreviation ifpred p n := (if p then pred n else n%nat).
+Abbreviation ifpred p n := (if p then pred n else n%_nat).
 
 Definition treeify_invariant size (f:treeify_t) :=
  forall acc,