From 7c161dc3e2c1b4ac442c40cbbdbc01c43c82f0bf Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 15 Jul 2024 14:55:38 +0200 Subject: [PATCH] Remove MathComp 2.1.0 deprecations --- theories/posnum.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/posnum.v b/theories/posnum.v index cf804f2..2a2adc2 100644 --- a/theories/posnum.v +++ b/theories/posnum.v @@ -132,7 +132,7 @@ Lemma posnum_lt0 x : (x%:num < 0 :> R) = false. Proof. by rewrite ltNge posnum_ge0. Qed. Lemma min_pos_gt0 x y : 0 < minr x%:num y%:num. -Proof. by rewrite lt_minr !posnum_gt0. Qed. +Proof. by rewrite lt_min !posnum_gt0. Qed. Canonical minr_posnum x y := PosNum (@min_pos_gt0 x y). End PosNumReal.