diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index f44e3f3c423cd7681048541f839c090117237e64..45559286228f8fcf71b137b1da25b91e99557acf 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -781,7 +781,7 @@ Record rFunctor := RFunctor {
     CmraMorphism (rFunctor_map fg)
 }.
 Existing Instances rFunctor_ne rFunctor_mor.
-Instance: Params (@rFunctor_map) 5 := {}.
+Instance: Params (@rFunctor_map) 9 := {}.
 
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
@@ -818,7 +818,7 @@ Record urFunctor := URFunctor {
     CmraMorphism (urFunctor_map fg)
 }.
 Existing Instances urFunctor_ne urFunctor_mor.
-Instance: Params (@urFunctor_map) 5 := {}.
+Instance: Params (@urFunctor_map) 9 := {}.
 
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 52bc4c554c43c52e7f998fe34772d916beda83dd..3bded308f0628a9d89e42cbd54a993c1b31fdbfd 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -676,7 +676,7 @@ Record cFunctor := CFunctor {
     cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
 }.
 Existing Instance cFunctor_ne.
-Instance: Params (@cFunctor_map) 5 := {}.
+Instance: Params (@cFunctor_map) 9 := {}.
 
 Delimit Scope cFunctor_scope with CF.
 Bind Scope cFunctor_scope with cFunctor.