From 1d98d4acf46a8d59bcf3cde073b8f107a0143f05 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Jan 2019 09:57:22 +0100
Subject: [PATCH] Fix  typo.

---
 theories/relations.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/relations.v b/theories/relations.v
index a67e7535..8577f9ce 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.
-- 
GitLab