diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index bfaf99b2ddaedf275b8462685e18f35fcdfeeb56..82abe8a6d67a5aed488229db868a7c2e7bdb4f0a 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -29,7 +29,7 @@ Section cofe.
 
   (* A good way of understanding this defintion of the uPred OFE is to
      consider the OFE uPred0 of monotonous SProp predicates. That is,
-     uPred0 is the OFE of non-expanding functions from M to SProp that
+     uPred0 is the OFE of non-expansive functions from M to SProp that
      are monotonous with respect to CMRA inclusion. This notion of
      monotonicity has to be stated in the SProp logic. It is exactly
      uPred_mono.