diff --git a/.nix/config.nix b/.nix/config.nix
index 4041d330f..ef948d907 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -3,7 +3,7 @@ let
     mathcomp-classical.job = true;
     mathcomp-reals.job = true;
     mathcomp-analysis.job = true;
-    mathcomp-altreals.job = true;
+    mathcomp-experimental-reals.job = true;
     mathcomp-reals-stdlib.job = true;
     mathcomp-analysis-stdlib.job = true;
     ssprove.job = false;
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2b9213098..743c396cc 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -20,7 +20,7 @@
 - in file `separation_axioms.v`,
   + new lemmas `compact_normal_local`, and `compact_normal`.
 
-- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals`
+- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals`
   with files
   + `xfinmap.v`
   + `discrete.v`
diff --git a/_CoqProject b/_CoqProject
index 4a9bd2415..febad3bd7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,7 +1,7 @@
 -Q classical mathcomp.classical
 -Q reals mathcomp.reals
 -Q reals_stdlib mathcomp.reals_stdlib
--Q altreals mathcomp.altreals
+-Q experimental_reals mathcomp.experimental_reals
 -Q theories mathcomp.analysis
 -Q analysis_stdlib mathcomp.analysis_stdlib
 
@@ -32,11 +32,11 @@ reals/itv.v
 reals/prodnormedzmodule.v
 reals/nsatz_realtype.v
 reals/all_reals.v
-altreals/xfinmap.v
-altreals/discrete.v
-altreals/realseq.v
-altreals/realsum.v
-altreals/distr.v
+experimental_reals/xfinmap.v
+experimental_reals/discrete.v
+experimental_reals/realseq.v
+experimental_reals/realsum.v
+experimental_reals/distr.v
 reals_stdlib/Rstruct.v
 theories/all_analysis.v
 theories/landau.v
diff --git a/coq-mathcomp-altreals.opam b/coq-mathcomp-experimental-reals.opam
similarity index 86%
rename from coq-mathcomp-altreals.opam
rename to coq-mathcomp-experimental-reals.opam
index 41c7c1a1e..017951fdc 100644
--- a/coq-mathcomp-altreals.opam
+++ b/coq-mathcomp-experimental-reals.opam
@@ -12,8 +12,8 @@ description: """
 This repository contains a library for alternative real numbers for
 the Coq proof-assistant and using the Mathematical Components library."""
 
-build: [make "-C" "altreals" "-j%{jobs}%"]
-install: [make "-C" "altreals" "install"]
+build: [make "-C" "experimental_reals" "-j%{jobs}%"]
+install: [make "-C" "experimental_reals" "install"]
 depends: [
   "coq-mathcomp-reals" { = version}
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
@@ -23,7 +23,7 @@ tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
   "keyword:reals"
-  "logpath:mathcomp.altreals"
+  "logpath:mathcomp.experimental_reals"
 ]
 authors: [
   "Reynald Affeldt"
diff --git a/altreals/LICENSE b/experimental_reals/LICENSE
similarity index 100%
rename from altreals/LICENSE
rename to experimental_reals/LICENSE
diff --git a/altreals/Make b/experimental_reals/Make
similarity index 88%
rename from altreals/Make
rename to experimental_reals/Make
index 85e6747e8..5d0d192b8 100644
--- a/altreals/Make
+++ b/experimental_reals/Make
@@ -1,4 +1,4 @@
--Q . mathcomp.altreals
+-Q . mathcomp.experimental_reals
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
diff --git a/altreals/Makefile b/experimental_reals/Makefile
similarity index 100%
rename from altreals/Makefile
rename to experimental_reals/Makefile
diff --git a/altreals/dedekind.v b/experimental_reals/dedekind.v
similarity index 100%
rename from altreals/dedekind.v
rename to experimental_reals/dedekind.v
diff --git a/altreals/discrete.v b/experimental_reals/discrete.v
similarity index 100%
rename from altreals/discrete.v
rename to experimental_reals/discrete.v
diff --git a/altreals/distr.v b/experimental_reals/distr.v
similarity index 100%
rename from altreals/distr.v
rename to experimental_reals/distr.v
diff --git a/altreals/realseq.v b/experimental_reals/realseq.v
similarity index 100%
rename from altreals/realseq.v
rename to experimental_reals/realseq.v
diff --git a/altreals/realsum.v b/experimental_reals/realsum.v
similarity index 100%
rename from altreals/realsum.v
rename to experimental_reals/realsum.v
diff --git a/altreals/xfinmap.v b/experimental_reals/xfinmap.v
similarity index 100%
rename from altreals/xfinmap.v
rename to experimental_reals/xfinmap.v