diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 7cb4ce262ec86924642b8bc1bbf768704b890800..33bd7151c74a68fda34eb77457e31deca9abb97a 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -956,7 +956,7 @@ Proof.
 Qed.
 
 (** Sigma *)
-Class LimitPreserving {A : ofeT} `{!Cofe A} (P : A → Prop) : Prop :=
+Class LimitPreserving `{!Cofe A} (P : A → Prop) : Prop :=
   limit_preserving : ∀ c : chain A, (∀ n, P (c n)) → P (compl c).
 
 Section sigma.
@@ -987,7 +987,7 @@ Section sigma.
   Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
 
   (* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving
-     suddenyl becomes explicit...? *)
+     suddenly becomes explicit...? *)
   Program Definition sig_compl `{LimitPreserving _ P} : Compl sigC :=
     λ c, exist P (compl (chain_map proj1_sig c)) _.
   Next Obligation.
@@ -1009,7 +1009,7 @@ Section sigma.
   Qed.
 End sigma.
 
-Arguments sigC {A} P.
+Arguments sigC {_} _.
 
 (** Notation for writing functors *)
 Notation "∙" := idCF : cFunctor_scope.