diff options
| author | Cyril Cohen <cohen@crans.org> | 2019-05-23 15:45:28 +0200 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2019-06-03 15:23:35 +0000 |
| commit | 547466064e465f64474b0e0c299e5eb7310be984 (patch) | |
| tree | b080f69939fc06e3c3a4e55dc9c790c27c734df6 /pkgs/top-level/coq-packages.nix | |
| parent | ddaf94d80483c8989cd7e1569df40215fee7b16c (diff) | |
coqPackages.mathcomp: 1.8.0 -> 1.9.0 and adding real-closed
Diffstat (limited to 'pkgs/top-level/coq-packages.nix')
| -rw-r--r-- | pkgs/top-level/coq-packages.nix | 43 |
1 files changed, 30 insertions, 13 deletions
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 9a1bdb07d5b9..cc40f78875c8 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -36,21 +36,38 @@ let ltac2 = callPackage ../development/coq-modules/ltac2 {}; math-classes = callPackage ../development/coq-modules/math-classes { }; inherit (callPackage ../development/coq-modules/mathcomp { }) - mathcompGen mathcompGenSingle mathcompCorePkgs_1_7 mathcompCorePkgs_1_8 mathcompCorePkgs - mathcomp mathcomp_1_7 mathcomp_1_8 ssreflect - mathcomp-ssreflect mathcomp-ssreflect_1_7 mathcomp-ssreflect_1_8 - mathcomp-fingroup mathcomp-fingroup_1_7 mathcomp-fingroup_1_8 - mathcomp-algebra mathcomp-algebra_1_7 mathcomp-algebra_1_8 - mathcomp-solvable mathcomp-solvable_1_7 mathcomp-solvable_1_8 - mathcomp-field mathcomp-field_1_7 mathcomp-field_1_8 - mathcomp-character mathcomp-character_1_7 mathcomp-character_1_8; + mathcompGen mathcompGenSingle ssreflect + + mathcompCorePkgs mathcomp + mathcomp-ssreflect mathcomp-fingroup mathcomp-algebra + mathcomp-solvable mathcomp-field mathcomp-character + + mathcompCorePkgs_1_7 mathcomp_1_7 + mathcomp-ssreflect_1_7 mathcomp-fingroup_1_7 mathcomp-algebra_1_7 + mathcomp-solvable_1_7 mathcomp-field_1_7 mathcomp-character_1_7 + + mathcompCorePkgs_1_8 mathcomp_1_8 + mathcomp-ssreflect_1_8 mathcomp-fingroup_1_8 mathcomp-algebra_1_8 + mathcomp-solvable_1_8 mathcomp-field_1_8 mathcomp-character_1_8 + + mathcompCorePkgs_1_9 mathcomp_1_9 + mathcomp-ssreflect_1_9 mathcomp-fingroup_1_9 mathcomp-algebra_1_9 + mathcomp-solvable_1_9 mathcomp-field_1_9 mathcomp-character_1_9; inherit (callPackage ../development/coq-modules/mathcomp/extra.nix { }) - mathcompExtraGen - mathcomp-finmap mathcomp-bigenough mathcomp-analysis mathcomp-multinomials - mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis mathcomp_1_7-multinomials + mathcompExtraGen multinomials + + mathcomp-finmap mathcomp-bigenough mathcomp-analysis + mathcomp-multinomials mathcomp-real-closed + + mathcomp_1_7-finmap mathcomp_1_7-bigenough mathcomp_1_7-analysis + mathcomp_1_7-multinomials mathcomp_1_7-real-closed mathcomp_1_7-finmap_1_0 - mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis mathcomp_1_8-multinomials - multinomials; + + mathcomp_1_8-finmap mathcomp_1_8-bigenough mathcomp_1_8-analysis + mathcomp_1_8-multinomials mathcomp_1_8-real-closed + + mathcomp_1_9-finmap mathcomp_1_9-bigenough mathcomp_1_9-analysis + mathcomp_1_9-multinomials mathcomp_1_9-real-closed; metalib = callPackage ../development/coq-modules/metalib { }; paco = callPackage ../development/coq-modules/paco {}; paramcoq = callPackage ../development/coq-modules/paramcoq {}; |