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

(cherry picked from commit 36d1ce50a7)
This commit is contained in:
Pierre Roux 2026-06-17 08:03:21 +02:00 committed by github-actions[bot]
commit 64299d2f37
2 changed files with 2 additions and 2 deletions

View file

@ -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 [

View file

@ -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 =