diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 1568c9917f5f2a101f72ab072725171ad2f57296..8f7f0b84afcb0c435aefa7fbf03d567d93f9320c 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -11,7 +11,7 @@ Set Primitive Projections.
     cases, we do not even need non-expansiveness.
 *)
 
-(** Unbundeled version *)
+(** Unbundled version *)
 Class Dist A := dist : nat → relation A.
 Instance: Params (@dist) 3 := {}.
 Notation "x ≡{ n }≡ y" := (dist n x y)
@@ -43,7 +43,7 @@ Record OfeMixin A `{Equiv A, Dist A} := {
   mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y
 }.
 
-(** Bundeled version *)
+(** Bundled version *)
 Structure ofeT := OfeT {
   ofe_car :> Type;
   ofe_equiv : Equiv ofe_car;