diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index a04889cbfe541401bbd41057787e032f0123b598..0009314dda6b22dc7e997d03660c4e385153940f 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -320,7 +320,7 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
    This means that CAS is atomic (it always reducs to an irreducible
    expression), but not strongly atomic (it does not always reduce to a value).
 
-   If there is a concurrent non-atomic write, the CAS itself is stuck: All it's
+   If there is a concurrent non-atomic write, the CAS itself is stuck: All its
    reductions are blocked.  *)
 | CasStuckS l n e1 lit1 e2 lit2 litl σ :
     to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →