rocqPackages.mathcomp-analysis: now depends on real-closed

2026-06-17 13:23:46 +02:00
parent 499d913a1a
commit 36d1ce50a7
2 changed files with 2 additions and 2 deletions
@@ -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 [
@@ -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 =