diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index b83234e00dd1f5a26f133a83cbe997349dc5fcfe..a04889cbfe541401bbd41057787e032f0123b598 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -317,6 +317,9 @@ Inductive head_step : expr → state → expr → state → list expr → Prop :
    state being stuck like we could in a language where failing and succeeding
    CAS are mutually exclusive.
 
+   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
    reductions are blocked.  *)
 | CasStuckS l n e1 lit1 e2 lit2 litl σ :