From 2beed39416a2df3abf0f4da3eccd736b23dc8cff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 May 2019 20:27:42 +0200
Subject: [PATCH] Fix typo.

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

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index f62241eab..cf7a5d31b 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -7,7 +7,7 @@ Local Arguments op _ _ _ !_ /.
 Local Arguments pcore _ _ !_ /.
 
 (** Define an agreement construction such that Agree A is discrete when A is discrete.
-    Notice that this construction is NOT complete.  The fullowing is due to AleÅ¡:
+    Notice that this construction is NOT complete.  The following is due to AleÅ¡:
 
 Proposition: Ag(T) is not necessarily complete.
 Proof.
-- 
GitLab