Adapt to math-comp/math-comp#1237

math-comp · Jul 5, 2024 · b07aa93 · b07aa93
1 parent 31e0216
commit b07aa93
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/xmathcomp/algR.v b/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.
 
@@ -72,7 +72,7 @@ set n := floorC _; have [n_lt0|n_ge0] := ltP n 0.
 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} :=