From f4b812a514fb1a39769540aa7178f39cd3e5b2b0 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 6 Dec 2021 10:37:33 -0500
Subject: [PATCH] Avoid using Min and Max, deprecated in v8.16
---
iris/algebra/numbers.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index a04152916..349be4dfd 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -69,7 +69,7 @@ Section max_nat.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite max_nat_op. by rewrite Nat.max_assoc.
- intros [x] [y]. by rewrite max_nat_op Nat.max_comm.
- - intros [x]. by rewrite max_nat_op Max.max_idempotent.
+ - intros [x]. by rewrite max_nat_op Nat.max_id.
Qed.
Canonical Structure max_natR : cmra := discreteR max_nat max_nat_ra_mixin.
@@ -124,7 +124,7 @@ Section min_nat.
apply ra_total_mixin; apply _ || eauto.
- intros [x] [y] [z]. repeat rewrite min_nat_op_min. by rewrite Nat.min_assoc.
- intros [x] [y]. by rewrite min_nat_op_min Nat.min_comm.
- - intros [x]. by rewrite min_nat_op_min Min.min_idempotent.
+ - intros [x]. by rewrite min_nat_op_min Nat.min_id.
Qed.
Canonical Structure min_natR : cmra := discreteR min_nat min_nat_ra_mixin.
@@ -147,7 +147,7 @@ Section min_nat.
Proof. done. Qed.
Global Instance : RightAbsorb (=) (MinNat 0) (â‹…).
- Proof. intros [x]. by rewrite min_nat_op_min Min.min_0_r. Qed.
+ Proof. intros [x]. by rewrite min_nat_op_min Nat.min_0_r. Qed.
Global Instance : IdemP (=@{min_nat}) (â‹…).
Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.
--
GitLab