diff --git a/theories/relations.v b/theories/relations.v
index a67e7535077fa2eb0f146b2da721d82e57fbb53f..8577f9ce9ec3403e9f0cbdc8351dcf418aaab127 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -33,7 +33,7 @@ Section definitions.
     | nsteps_O x : nsteps 0 x x
     | nsteps_l n x y z : R x y → nsteps n y z → nsteps (S n) x z.
 
-  (** Reduction of at most [n] steps. *)
+  (** Reductions of at most [n] steps. *)
   Inductive bsteps : nat → relation A :=
     | bsteps_refl n x : bsteps n x x
     | bsteps_l n x y z : R x y → bsteps n y z → bsteps (S n) x z.