From 9333e8d26855176f25ac4397d8fe2e8b7f1720ef Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 5 Sep 2020 11:11:08 +0200
Subject: [PATCH] use lia instead of omega
---
theories/typing/lib/rwlock/rwlock_code.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 227757d1..17576c1b 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -246,7 +246,7 @@ Section rwlock_functions.
iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
iModIntro.
destruct st2 as [[[]|[[ν q] n]]|]; simpl in Eqst2.
- - exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. omega.
+ - exfalso. clear -Eqst2 Hm1. rewrite Eqst2 in Hm1. lia.
- rewrite Eqst2. iDestruct "INT" as "[$ INT]".
iExists (). iSplitL ""; [done|]. iIntros (t2 Ext2) "W' !>". iSplitL "".
{ rewrite /Q1 Eqst2. by iIntros "!> $". } iIntros "!> !>".
--
GitLab