From 8e376c4fbecc60bac12f89dbdfb8bca869bb6100 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 12 Jun 2026 17:03:35 +0900 Subject: [PATCH 1/2] rocqPackages.mathcomp-analysis: update dependencies --- pkgs/development/coq-modules/mathcomp-analysis/default.nix | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix index 0df390b8a9ee..3b366df94276 100644 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -84,7 +84,10 @@ let "classical" = [ ]; "reals" = [ "classical" ]; "experimental-reals" = [ "reals" ]; - "analysis" = [ "reals" ]; + "analysis" = [ + "reals" + "real-closed" + ]; "reals-stdlib" = [ "reals" ]; "analysis-stdlib" = [ "analysis" From da9109b99c89b9928c6bf994eff41c93e4b69be2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 15 Jun 2026 15:35:29 +0900 Subject: [PATCH 2/2] ocqPackages.mathcomp-analysis: change how to specify dependencies --- pkgs/development/coq-modules/mathcomp-analysis/default.nix | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix index 3b366df94276..be83ed4778a9 100644 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -4,6 +4,7 @@ mathcomp, mathcomp-finmap, mathcomp-bigenough, + mathcomp-real-closed, hierarchy-builder, stdlib, single ? false, @@ -84,10 +85,7 @@ let "classical" = [ ]; "reals" = [ "classical" ]; "experimental-reals" = [ "reals" ]; - "analysis" = [ - "reals" - "real-closed" - ]; + "analysis" = [ "reals" ]; "reals-stdlib" = [ "reals" ]; "analysis-stdlib" = [ "analysis" @@ -107,6 +105,7 @@ let analysis-deps = [ mathcomp.field mathcomp-bigenough + mathcomp-real-closed ]; intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package}); pkgpath = lib.switch package [