Merge pull request #25 from coq-community/cleanup-deprecations

Remove MathComp 2.1.0 deprecations
coq-community · Jul 15, 2024 · 910f96b · 910f96b
2 parents 3b24987 + 7c161dc
commit 910f96b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.