diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index 191972664b33..58c51c150e37 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -54,7 +54,7 @@ let
   packages = {
     "classical" = [];
     "reals" = [ "classical" ];
-    "altreals" = [ "reals" ];
+    "experimental-reals" = [ "reals" ];
     "analysis" = [ "reals" ];
     "reals-stdlib" = [ "reals" ];
     "analysis-stdlib" = [ "analysis" "reals-stdlib" ];
@@ -62,12 +62,13 @@ let
 
   mathcomp_ = package: let
       classical-deps = [ mathcomp.algebra mathcomp-finmap ];
-      altreals-deps = [ mathcomp-bigenough ];
+      experimental-reals-deps = [ mathcomp-bigenough ];
       analysis-deps = [ mathcomp.field mathcomp-bigenough ];
       intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
       pkgpath = lib.switch package [
         { case = "single"; out = "."; }
         { case = "analysis"; out = "theories"; }
+        { case = "experimental-reals"; out = "experimental_reals"; }
         { case = "reals-stdlib"; out = "reals_stdlib"; }
         { case = "analysis-stdlib"; out = "analysis_stdlib"; }
       ] package;
@@ -81,7 +82,7 @@ let
         propagatedBuildInputs =
           intra-deps
           ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps
-          ++ lib.optionals (lib.elem package [ "altreals" "single" ]) altreals-deps
+          ++ lib.optionals (lib.elem package [ "experimental-reals" "single" ]) experimental-reals-deps
           ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps;
 
         preBuild = ''
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index cfdfe93f4462..0181ceb3da71 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -99,12 +99,12 @@ let
       mathcomp-character = self.mathcomp.character;
       mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel {};
       mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics {};
-      mathcomp-altreals = self.mathcomp-analysis.altreals;
       mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};
       mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
       mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery {};
       mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};
       mathcomp-classical = self.mathcomp-analysis.classical;
+      mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
       mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {};
       mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo {};
       mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};