From b27fc190cb9816d27c844ed1c868e083c0691876 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 16 May 2019 16:58:08 +0200
Subject: [PATCH] fix for upcoming precedence change in Coq

---
 theories/lang/races.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/lang/races.v b/theories/lang/races.v
index 1423c77f..79da2aa6 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -86,9 +86,9 @@ Lemma next_access_head_reducible_state e σ a l :
   next_access_head e σ a l → head_reducible e σ →
   head_reduce_not_to_stuck e σ →
   match a with
-  | (ReadAcc, ScOrd | Na1Ord) => ∃ v n, σ !! l = Some (RSt n, v)
+  | (ReadAcc, (ScOrd | Na1Ord)) => ∃ v n, σ !! l = Some (RSt n, v)
   | (ReadAcc, Na2Ord) => ∃ v n, σ !! l = Some (RSt (S n), v)
-  | (WriteAcc, ScOrd | Na1Ord) => ∃ v, σ !! l = Some (RSt 0, v)
+  | (WriteAcc, (ScOrd | Na1Ord)) => ∃ v, σ !! l = Some (RSt 0, v)
   | (WriteAcc, Na2Ord) => ∃ v, σ !! l = Some (WSt, v)
   | (FreeAcc, _) => ∃ v ls, σ !! l = Some (ls, v)
   end.
-- 
GitLab