diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index a5f0b688836ee34b189848b05d7444bc9ecb1a32..235fb97b4222bcb19fd8b7ab73f1eb33842ee52b 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type".
   for this is that it makes curried functions usable: Given a WP for [f a b], we
   know that any effects [f] might have to not matter until after *both* [a] and
   [b] are evaluated.  With left-to-right evaluation, that triple is basically
-  useless the user let-expands [b].
+  useless unless the user let-expands [b].
 
 *)