From 408b55f0d6372fefa9244ab5f6d4035132fb3f97 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 Jun 2019 23:29:11 +0200
Subject: [PATCH] comment nits

---
 theories/heap_lang/lang.v     | 2 +-
 theories/heap_lang/notation.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index cb8303086..84ac31eac 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 861b4a17d..07e5df432 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
-- 
GitLab