From 09e39b6784573dc78e9cef4b65c5552c1f1bfd79 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 29 Oct 2017 14:15:47 +0100
Subject: [PATCH] fix typo

---
 theories/lang/lang.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index a04889cb..0009314d 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 →
-- 
GitLab