pyrox.dev / nixpkgs
lol
fork atom

Refine dependencies from mathcomp-ssreflect to mathcomp-boot

authored by

Pierre Roux and committed by
Vincent Laporte e95a2343 0401f9a2

+33 -31
+3 -3
pkgs/development/coq-modules/QuickChick/default.nix
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 - ssreflect, 6 ExtLib, 7 simple-io, 8 version ? null, ··· 17 inherit version; 18 defaultVersion = 19 lib.switch 20 - [ coq.coq-version ssreflect.version ] 21 [ 22 { 23 cases = [ ··· 127 mlPlugin = true; 128 nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild; 129 propagatedBuildInputs = 130 - [ ssreflect ] 131 ++ lib.optionals recent [ 132 ExtLib 133 simple-io
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 + mathcomp-boot, 6 ExtLib, 7 simple-io, 8 version ? null, ··· 17 inherit version; 18 defaultVersion = 19 lib.switch 20 + [ coq.coq-version mathcomp-boot.version ] 21 [ 22 { 23 cases = [ ··· 127 mlPlugin = true; 128 nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild; 129 propagatedBuildInputs = 130 + [ mathcomp-boot ] 131 ++ lib.optionals recent [ 132 ExtLib 133 simple-io
+2 -2
pkgs/development/coq-modules/autosubst/default.nix
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 - mathcomp-ssreflect, 6 stdlib, 7 version ? null, 8 }: ··· 35 ] null; 36 37 propagatedBuildInputs = [ 38 - mathcomp-ssreflect 39 stdlib 40 ]; 41
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 + mathcomp-boot, 6 stdlib, 7 version ? null, 8 }: ··· 35 ] null; 36 37 propagatedBuildInputs = [ 38 + mathcomp-boot 39 stdlib 40 ]; 41
+2 -2
pkgs/development/coq-modules/coquelicot/default.nix
··· 4 autoconf, 5 coq, 6 stdlib, 7 - ssreflect, 8 version ? null, 9 }: 10 ··· 59 nativeBuildInputs = [ autoconf ]; 60 propagatedBuildInputs = [ 61 stdlib 62 - ssreflect 63 ]; 64 useMelquiondRemake.logpath = "Coquelicot"; 65
··· 4 autoconf, 5 coq, 6 stdlib, 7 + mathcomp-boot, 8 version ? null, 9 }: 10 ··· 59 nativeBuildInputs = [ autoconf ]; 60 propagatedBuildInputs = [ 61 stdlib 62 + mathcomp-boot 63 ]; 64 useMelquiondRemake.logpath = "Coquelicot"; 65
+3 -3
pkgs/development/coq-modules/extructures/default.nix
··· 3 mkCoqDerivation, 4 coq, 5 version ? null, 6 - ssreflect, 7 deriving, 8 }: 9 ··· 15 defaultVersion = 16 with lib.versions; 17 lib.switch 18 - [ coq.coq-version ssreflect.version ] 19 [ 20 { 21 cases = [ ··· 63 release."0.3.0".sha256 = "sha256:14rm0726f1732ldds495qavg26gsn30w6dfdn36xb12g5kzavp38"; 64 release."0.2.2".sha256 = "sha256:1clzza73gccy6p6l95n6gs0adkqd3h4wgl4qg5l0qm4q140grvm7"; 65 66 - propagatedBuildInputs = [ ssreflect ]; 67 68 meta = with lib; { 69 description = "Finite data structures with extensional reasoning";
··· 3 mkCoqDerivation, 4 coq, 5 version ? null, 6 + mathcomp-boot, 7 deriving, 8 }: 9 ··· 15 defaultVersion = 16 with lib.versions; 17 lib.switch 18 + [ coq.coq-version mathcomp-boot.version ] 19 [ 20 { 21 cases = [ ··· 63 release."0.3.0".sha256 = "sha256:14rm0726f1732ldds495qavg26gsn30w6dfdn36xb12g5kzavp38"; 64 release."0.2.2".sha256 = "sha256:1clzza73gccy6p6l95n6gs0adkqd3h4wgl4qg5l0qm4q140grvm7"; 65 66 + propagatedBuildInputs = [ mathcomp-boot ]; 67 68 meta = with lib; { 69 description = "Finite data structures with extensional reasoning";
+2 -2
pkgs/development/coq-modules/fourcolor/default.nix
··· 64 null; 65 66 propagatedBuildInputs = [ 67 - mathcomp.algebra 68 - mathcomp.ssreflect 69 mathcomp.fingroup 70 ]; 71 72 meta = with lib; {
··· 64 null; 65 66 propagatedBuildInputs = [ 67 + mathcomp.boot 68 mathcomp.fingroup 69 + mathcomp.algebra 70 ]; 71 72 meta = with lib; {
+2 -2
pkgs/development/coq-modules/gaia/default.nix
··· 50 null; 51 52 propagatedBuildInputs = [ 53 - mathcomp.ssreflect 54 - mathcomp.algebra 55 mathcomp.fingroup 56 stdlib 57 ]; 58
··· 50 null; 51 52 propagatedBuildInputs = [ 53 + mathcomp.boot 54 mathcomp.fingroup 55 + mathcomp.algebra 56 stdlib 57 ]; 58
+2 -2
pkgs/development/coq-modules/interval/default.nix
··· 5 coq, 6 coquelicot, 7 flocq, 8 - mathcomp-ssreflect, 9 mathcomp-fingroup, 10 bignums ? null, 11 gnuplot_qt, ··· 82 ++ [ 83 coquelicot 84 flocq 85 - mathcomp-ssreflect 86 mathcomp-fingroup 87 ] 88 ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
··· 5 coq, 6 coquelicot, 7 flocq, 8 + mathcomp-boot, 9 mathcomp-fingroup, 10 bignums ? null, 11 gnuplot_qt, ··· 82 ++ [ 83 coquelicot 84 flocq 85 + mathcomp-boot 86 mathcomp-fingroup 87 ] 88 ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
+2
pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 mathcomp-algebra, 6 coq-elpi, 7 mathcomp-zify, ··· 60 release."1.2.4".sha256 = "sha256-BRxt0LGPz2u3kJRjcderaZqCfs8M8qKAAwNSWmIck7Q="; 61 62 propagatedBuildInputs = [ 63 mathcomp-algebra 64 coq-elpi 65 mathcomp-zify
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 + mathcomp-ssreflect, 6 mathcomp-algebra, 7 coq-elpi, 8 mathcomp-zify, ··· 61 release."1.2.4".sha256 = "sha256-BRxt0LGPz2u3kJRjcderaZqCfs8M8qKAAwNSWmIck7Q="; 62 63 propagatedBuildInputs = [ 64 + mathcomp-ssreflect 65 mathcomp-algebra 66 coq-elpi 67 mathcomp-zify
+2 -2
pkgs/development/coq-modules/mathcomp-bigenough/default.nix
··· 1 { 2 coq, 3 mkCoqDerivation, 4 - mathcomp, 5 lib, 6 version ? null, 7 }: ··· 34 } 35 ] null; 36 37 - propagatedBuildInputs = [ mathcomp.ssreflect ]; 38 39 meta = { 40 description = "Small library to do epsilon - N reasonning";
··· 1 { 2 coq, 3 mkCoqDerivation, 4 + mathcomp-boot, 5 lib, 6 version ? null, 7 }: ··· 34 } 35 ] null; 36 37 + propagatedBuildInputs = [ mathcomp-boot ]; 38 39 meta = { 40 description = "Small library to do epsilon - N reasonning";
+3 -3
pkgs/development/coq-modules/mathcomp-finmap/default.nix
··· 1 { 2 coq, 3 mkCoqDerivation, 4 - mathcomp, 5 lib, 6 version ? null, 7 }: ··· 18 defaultVersion = 19 with lib.versions; 20 lib.switch 21 - [ coq.version mathcomp.version ] 22 [ 23 { 24 cases = [ ··· 107 "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa"; 108 }; 109 110 - propagatedBuildInputs = [ mathcomp.ssreflect ]; 111 112 meta = { 113 description = "Finset and finmap library";
··· 1 { 2 coq, 3 mkCoqDerivation, 4 + mathcomp-boot, 5 lib, 6 version ? null, 7 }: ··· 18 defaultVersion = 19 with lib.versions; 20 lib.switch 21 + [ coq.version mathcomp-boot.version ] 22 [ 23 { 24 cases = [ ··· 107 "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa"; 108 }; 109 110 + propagatedBuildInputs = [ mathcomp-boot ]; 111 112 meta = { 113 description = "Finset and finmap library";
+3 -3
pkgs/development/coq-modules/mathcomp-zify/default.nix
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 - mathcomp-algebra, 6 - mathcomp-ssreflect, 7 mathcomp-fingroup, 8 stdlib, 9 version ? null, 10 }: ··· 54 release."1.5.0+2.0+8.16".sha256 = "sha256-boBYGvXdGFc6aPnjgSZYSoW4kmN5khtNrSV3DUv9DqM="; 55 56 propagatedBuildInputs = [ 57 mathcomp-algebra 58 - mathcomp-ssreflect 59 mathcomp-fingroup 60 stdlib 61 ];
··· 2 lib, 3 mkCoqDerivation, 4 coq, 5 + mathcomp-boot, 6 mathcomp-fingroup, 7 + mathcomp-algebra, 8 stdlib, 9 version ? null, 10 }: ··· 54 release."1.5.0+2.0+8.16".sha256 = "sha256-boBYGvXdGFc6aPnjgSZYSoW4kmN5khtNrSV3DUv9DqM="; 55 56 propagatedBuildInputs = [ 57 + mathcomp-boot 58 mathcomp-algebra 59 mathcomp-fingroup 60 stdlib 61 ];
+1 -1
pkgs/development/coq-modules/multinomials/default.nix
··· 138 ''; 139 140 propagatedBuildInputs = [ 141 - mathcomp.ssreflect 142 mathcomp.algebra 143 mathcomp-finmap 144 mathcomp.fingroup
··· 138 ''; 139 140 propagatedBuildInputs = [ 141 + mathcomp.boot 142 mathcomp.algebra 143 mathcomp-finmap 144 mathcomp.fingroup
+1 -1
pkgs/development/coq-modules/odd-order/default.nix
··· 39 40 propagatedBuildInputs = [ 41 mathcomp.character 42 - mathcomp.ssreflect 43 mathcomp.fingroup 44 mathcomp.algebra 45 mathcomp.solvable
··· 39 40 propagatedBuildInputs = [ 41 mathcomp.character 42 + mathcomp.boot 43 mathcomp.fingroup 44 mathcomp.algebra 45 mathcomp.solvable
+2 -2
pkgs/development/coq-modules/relation-algebra/default.nix
··· 3 mkCoqDerivation, 4 coq, 5 aac-tactics, 6 - mathcomp, 7 version ? null, 8 }: 9 ··· 79 80 propagatedBuildInputs = [ 81 aac-tactics 82 - mathcomp.ssreflect 83 ]; 84 85 meta = with lib; {
··· 3 mkCoqDerivation, 4 coq, 5 aac-tactics, 6 + mathcomp-boot, 7 version ? null, 8 }: 9 ··· 79 80 propagatedBuildInputs = [ 81 aac-tactics 82 + mathcomp-boot 83 ]; 84 85 meta = with lib; {
+3 -3
pkgs/development/coq-modules/ssprove/default.nix
··· 4 coq, 5 version ? null, 6 equations, 7 - mathcomp-ssreflect, 8 mathcomp-analysis, 9 mathcomp-experimental-reals, 10 extructures, ··· 19 defaultVersion = 20 with lib.versions; 21 lib.switch 22 - [ coq.coq-version mathcomp-ssreflect.version ] 23 [ 24 { 25 cases = [ ··· 62 63 propagatedBuildInputs = [ 64 equations 65 - mathcomp-ssreflect 66 mathcomp-analysis 67 mathcomp-experimental-reals 68 extructures
··· 4 coq, 5 version ? null, 6 equations, 7 + mathcomp-boot, 8 mathcomp-analysis, 9 mathcomp-experimental-reals, 10 extructures, ··· 19 defaultVersion = 20 with lib.versions; 21 lib.switch 22 + [ coq.coq-version mathcomp-boot.version ] 23 [ 24 { 25 cases = [ ··· 62 63 propagatedBuildInputs = [ 64 equations 65 + mathcomp-boot 66 mathcomp-analysis 67 mathcomp-experimental-reals 68 extructures