diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 1ae544dbc013992eb418e9407de87cb33e5447ce..ef26c1a7745f5dea760d2393ab70a5d2dc389542 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -475,7 +475,7 @@ Proof.
     [done|by rewrite lookup_singleton].
 Qed.
 
-Lemma gmap_fmap_mono {B : ucmraT} (f : A → B) m1 m2 :
+Lemma gmap_fmap_mono {B : cmraT} (f : A → B) m1 m2 :
   Proper ((≡) ==> (≡)) f →
   (∀ x y, x ≼ y → f x ≼ f y) → m1 ≼ m2 → fmap f m1 ≼ fmap f m2.
 Proof.