From ffa7e1149686804aadae0d9c843d97c043756df9 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Thu, 5 Nov 2020 18:23:19 +0100
Subject: [PATCH] fix Z scope in arc_cmra

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

diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 596986c8..49478dc2 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -93,6 +93,7 @@ Definition Z_of_arcstrong_st (st : strong_stUR) : Z :=
   | Some (_, n) =>  Zpos n
   end.
 
+Local Open Scope Z_scope.
 
 Lemma strong_stUR_value st: 0 ≤ Z_of_arcstrong_st st.
 Proof. destruct st as [[]|]; simpl; lia. Qed.
-- 
GitLab