diff --git a/.github/workflows/nix-action-9.0-master.yml b/.github/workflows/nix-action-9.0-master.yml
index 758425db49..aba868db3f 100644
--- a/.github/workflows/nix-action-9.0-master.yml
+++ b/.github/workflows/nix-action-9.0-master.yml
@@ -491,7 +491,7 @@ jobs:
   mathcomp-experimental-reals:
     needs:
     - rocq-core
-    - mathcomp-reals
+    - mathcomp-analysis
     - mathcomp-bigenough
     runs-on: ubuntu-latest
     steps:
@@ -546,9 +546,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "9.0-master" --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-reals'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "9.0-master" --argstr job "mathcomp-reals"
+        "9.0-master" --argstr job "mathcomp-analysis"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
@@ -680,10 +680,6 @@ jobs:
       name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "9.0-master" --argstr job "mathcomp-analysis-stdlib"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-algebra-tactics'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "9.0-master" --argstr job "mathcomp-algebra-tactics"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: interval'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
diff --git a/.github/workflows/nix-action-9.1-master.yml b/.github/workflows/nix-action-9.1-master.yml
index 9424a3bb46..185797a8ee 100644
--- a/.github/workflows/nix-action-9.1-master.yml
+++ b/.github/workflows/nix-action-9.1-master.yml
@@ -491,7 +491,7 @@ jobs:
   mathcomp-experimental-reals:
     needs:
     - rocq-core
-    - mathcomp-reals
+    - mathcomp-analysis
     - mathcomp-bigenough
     runs-on: ubuntu-latest
     steps:
@@ -546,9 +546,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "9.1-master" --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-reals'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "9.1-master" --argstr job "mathcomp-reals"
+        "9.1-master" --argstr job "mathcomp-analysis"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
@@ -680,10 +680,6 @@ jobs:
       name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "9.1-master" --argstr job "mathcomp-analysis-stdlib"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-algebra-tactics'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "9.1-master" --argstr job "mathcomp-algebra-tactics"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: interval'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml
index 56b4542f8c..adb5918eec 100644
--- a/.github/workflows/nix-action-master.yml
+++ b/.github/workflows/nix-action-master.yml
@@ -617,7 +617,7 @@ jobs:
   mathcomp-experimental-reals:
     needs:
     - rocq-core
-    - mathcomp-reals
+    - mathcomp-analysis
     - mathcomp-bigenough
     runs-on: ubuntu-latest
     steps:
@@ -672,9 +672,9 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "master" --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-reals'
+      name: 'Building/fetching previous CI target: mathcomp-analysis'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "master" --argstr job "mathcomp-reals"
+        "master" --argstr job "mathcomp-analysis"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: mathcomp-bigenough'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
diff --git a/.nix/config.nix b/.nix/config.nix
index eff51f0ffb..7c48a67da2 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -8,6 +8,8 @@ let
     mathcomp-analysis-stdlib.job = true;
     ssprove.override.version = "main";
     mathcomp-infotheo.override.version = "master";
+    interval.override.version = "master";
+    coquelicot.override.version = "master";
   };
 in {
   ## DO NOT CHANGE THIS
@@ -59,6 +61,9 @@ in {
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.0";
+      mathcomp.override.version = "master";
+      mathcomp-bigenough.override.version = "master";
+      mathcomp-finmap.override.version = "master";
       ssprove.job = false;  # not yet available for 9.1
     };
   };
@@ -84,6 +89,9 @@ in {
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.1";
+      mathcomp.override.version = "master";
+      mathcomp-bigenough.override.version = "master";
+      mathcomp-finmap.override.version = "master";
       ssprove.job = false;  # not yet available for 9.1
     };
   };
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
index ff570aeca7..e70ee2f134 100644
--- a/.nix/coq-nix-toolbox.nix
+++ b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"6b32b8cd491ec44b75da86fb17e4353f2f102328"
+"4a441c50de5618ef066128f9f6f84e6bc13066da"
diff --git a/.nix/rocq-overlays/mathcomp-analysis-single/default.nix b/.nix/rocq-overlays/mathcomp-analysis-single/default.nix
index 9b8ebde669..1232b4bf47 100644
--- a/.nix/rocq-overlays/mathcomp-analysis-single/default.nix
+++ b/.nix/rocq-overlays/mathcomp-analysis-single/default.nix
@@ -1,2 +1,2 @@
-{ mathcomp-analysis }:
+{ mathcomp-analysis, ... }:
 mathcomp-analysis.override {single = true;}