From 36d1ce50a7839820c005c4d4e79dc5581bd52c1e Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 17 Jun 2026 08:03:21 +0200
Subject: [PATCH] rocqPackages.mathcomp-analysis: now depends on real-closed

---
 pkgs/development/coq-modules/mathcomp-analysis/default.nix  | 2 --
 pkgs/development/rocq-modules/mathcomp-analysis/default.nix | 2 ++
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index be83ed4778a9..0df390b8a9ee 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -4,7 +4,6 @@
   mathcomp,
   mathcomp-finmap,
   mathcomp-bigenough,
-  mathcomp-real-closed,
   hierarchy-builder,
   stdlib,
   single ? false,
@@ -105,7 +104,6 @@ let
       analysis-deps = [
         mathcomp.field
         mathcomp-bigenough
-        mathcomp-real-closed
       ];
       intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
       pkgpath = lib.switch package [
diff --git a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
index 1a77e673e4f7..c40340feeb35 100644
--- a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
@@ -4,6 +4,7 @@
   mathcomp,
   mathcomp-finmap,
   mathcomp-bigenough,
+  mathcomp-real-closed,
   stdlib,
   single ? false,
   rocq-core,
@@ -58,6 +59,7 @@ let
       analysis-deps = [
         mathcomp.field
         mathcomp-bigenough
+        mathcomp-real-closed
       ];
       intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
       pkgpath =