From c9597ff9ec323f469ab3d769f47bd2e81f1fcf73 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
Date: Tue, 2 Jul 2024 13:56:42 +0200
Subject: [PATCH] Treat a deprecation warning about Qint

---
 meta.yml            | 8 ++------
 theories/realprop.v | 4 ++--
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/meta.yml b/meta.yml
index 0d3bf59..3413273 100644
--- a/meta.yml
+++ b/meta.yml
@@ -38,10 +38,6 @@ supported_coq_versions:
   opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '2.0.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.18'
@@ -64,9 +60,9 @@ ci_cron_schedule: '0 5 * * *'
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.0.0" & < "2.3~") | (= "dev")}'
+    version: '{(>= "2.1.0" & < "2.3~") | (= "dev")}'
   description: |-
-    [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
diff --git a/theories/realprop.v b/theories/realprop.v
index ed9a2dc..8af8291 100644
--- a/theories/realprop.v
+++ b/theories/realprop.v
@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2018 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div order.
-From mathcomp Require Import ssralg ssrnum ssrint rat intdiv.
+From mathcomp Require Import ssralg ssrnum ssrint archimedean rat intdiv.
 From Coq Require Import Morphisms Setoid.
 From fourcolor Require Import real realsyntax.
 
@@ -46,7 +46,7 @@ Definition max x y : R := IF x >= y then x else y.
 Definition intR m : R := match m with Posz n => n%:R | Negz n => - n.+1%:R end.
 
 Definition ratR (a : rat) :=
-  if a \is a Qint then intR (numq a) else intR (numq a) / intR (denq a).
+  if a \is a Num.int then intR (numq a) else intR (numq a) / intR (denq a).
 
 Inductive floor_set x : Real.set R :=
   FloorSet m of intR m <= x : floor_set x (intR m).