diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index f62241eabbdbca72445d95887cd66ee1f7f93545..cf7a5d31bb64aabbe9dd42d346931c95db2ebb19 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.