Merge pull request #93 from pi8027/archimedean

Adapt to math-comp/math-comp#1237

.nix/config.nix

@@ -38,24 +38,26 @@
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
   bundles = let
-    gen = coqv: mcv:
-      { "coq${coqv}+mc${mcv}".coqPackages = {
-               coq.override.version = coqv;
-               mathcomp.override.version = mcv;
-               mathcomp.job = false;
+    gen = coqv: mcv: elpiv:
+      { "coq${coqv}+mc${mcv}" = {
+        coqPackages = {
+          coq.override.version = coqv;
+          mathcomp.override.version = mcv;
+          mathcomp.job = false;
         } // (if (coqv == "master") then {
-            coq-elpi.override.version = "coq-master";
-            hierarchy-builder.override.version = "master";
+          coq-elpi.override.version = "master";
+          hierarchy-builder.override.version = "master";
         } else {}) // {
-            mathcomp-real-closed.override.version = "master";
-            mathcomp-bigenough.override.version = "1.0.1";
+          mathcomp-real-closed.override.version = "master";
+          mathcomp-bigenough.override.version = "1.0.1";
         };
-      }; in
-    gen "8.16" "mathcomp-2.1.0" //
-    gen "8.17" "mathcomp-2.1.0" //
-    gen "8.18" "mathcomp-2.1.0" //
-    gen "8.19" "mathcomp-2.2.0" //
-    gen "master" "master";
+        ocamlPackages = if (elpiv != "") then { elpi.override.version = elpiv; } else {};
+      }; }; in
+    gen "8.16" "mathcomp-2.1.0" "" //
+    gen "8.17" "mathcomp-2.1.0" "" //
+    gen "8.18" "mathcomp-2.1.0" "" //
+    gen "8.19" "mathcomp-2.2.0" "" //
+    gen "master" "master" "1.19.2";
 
   ## Cachix caches to use in CI
   ## Below we list some standard ones

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"281be33f1e42a92e5c47f30907819aad1a45e5f2"
+"66abb687550ec2800bc1724036cfb5d9656c901c"

theories/xmathcomp/algR.v

@@ -1,5 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
+From mathcomp Require Import all_ssreflect all_fingroup all_algebra archimedean.
 From mathcomp Require Import all_solvable all_field.
 From Abel Require Import various.
 
@@ -63,16 +63,21 @@ HB.instance Definition _ := Num.isNumRing.Build algR
   algR_addr_gt0 algR_ger_leVge algR_normrM algR_ler_def.
 End Num.
 
+(* TODO: remove when dropping the support for MathComp 2.2 *)
+Local Fact real_floor_itv (R : archiNumDomainType) (x : R) :
+       x \is Num.real -> (Num.floor x)%:~R <= x < (Num.floor x + 1)%:~R.
+Proof. exact: real_floor_itv || exact: floor_itv. Qed.
+
 Definition algR_archiFieldMixin : Num.archimedean_axiom algR.
 Proof.
-move=> /= x; have /andP[/= _] := floorC_itv (valP `|x|).
-set n := floorC _; have [n_lt0|n_ge0] := ltP n 0.
+move=> /= x; have /andP[/= _] := real_floor_itv (valP `|x|).
+set n := Num.floor _; have [n_lt0|n_ge0] := ltP n 0.
   move=> /(@lt_le_trans _ _ _ _ 0); rewrite lerz0 lezD1.
   by move=> /(_ n_lt0); rewrite normr_lt0.
 move=> x_lt; exists (`|(n + 1)%R|%N); apply: lt_le_trans x_lt _.
 by rewrite /= rmorphMn/= pmulrn gez0_abs// addr_ge0.
 Qed.
-HB.instance Definition _ := Num.RealField_isArchimedean.Build algR
+HB.instance Definition _ := Num.NumDomain_bounded_isArchimedean.Build algR
   algR_archiFieldMixin.
 
 Definition algRpfactor (x : algC) : {poly algR} :=