diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index bd5f3e3867541643ed985bd443678d9a4fecda43..c32b4af9e7778e367d4964a7203bd7d2dbcc0e72 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -586,7 +586,7 @@ Section ofe_mor.
     intros ? c n x y Hx. by rewrite (conv_compl n (ofe_mor_chain c x))
       (conv_compl n (ofe_mor_chain c y)) /= Hx.
   Qed.
-  Global Program Instance ofe_more_cofe `{Cofe B} : Cofe ofe_morC :=
+  Global Program Instance ofe_mor_cofe `{Cofe B} : Cofe ofe_morC :=
     {| compl := ofe_mor_compl |}.
   Next Obligation.
     intros ? n c x; simpl.