diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index cb8303086f248dd33d823d3bbc735d0bab5eb28a..84ac31eac7fd4528ead83ab637f24118e4fa156f 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -97,7 +97,7 @@ Inductive expr :=
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
-  | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr)
+  | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
   | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
   (* Prophecy *)
   | NewProph
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 861b4a17dd16bc5bcfc327ae36a40303663c2bcd..07e5df43260a4ac277bf6ecb0b51b9d5b97c54db 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -25,7 +25,7 @@ Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
 Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
 Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
 Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
-(** Compare-and-set (CAS) retursn just a boolean indicating success or failure. *)
+(** Compare-and-set (CAS) returns just a boolean indicating success or failure. *)
 Notation CAS l e1 e2 := (Snd (CmpXchg l e1 e2)) (only parsing).
 
 (* Skip should be atomic, we sometimes open invariants around