summary refs log tree commit diff
path: root/pkgs/top-level/coq-packages.nix
diff options
context:
space:
mode:
authorCyril Cohen <cohen@crans.org>2019-05-23 15:45:28 +0200
committerVincent Laporte <Vincent.Laporte@gmail.com>2019-06-03 15:23:35 +0000
commit547466064e465f64474b0e0c299e5eb7310be984 (patch)
treeb080f69939fc06e3c3a4e55dc9c790c27c734df6 /pkgs/top-level/coq-packages.nix
parentddaf94d80483c8989cd7e1569df40215fee7b16c (diff)
downloadnixpkgs-547466064e465f64474b0e0c299e5eb7310be984.tar
nixpkgs-547466064e465f64474b0e0c299e5eb7310be984.tar.gz
nixpkgs-547466064e465f64474b0e0c299e5eb7310be984.tar.bz2
nixpkgs-547466064e465f64474b0e0c299e5eb7310be984.tar.lz
nixpkgs-547466064e465f64474b0e0c299e5eb7310be984.tar.xz
nixpkgs-547466064e465f64474b0e0c299e5eb7310be984.tar.zst
nixpkgs-547466064e465f64474b0e0c299e5eb7310be984.zip
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.nix43
1 files changed, 30 insertions, 13 deletions
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 9a1bdb07d5b..cc40f78875c 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 {};