Treat a deprecation warning about Qint

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: |-

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).