summary refs log tree commit diff
diff options
context:
space:
mode:
authorVincent Laporte <Vincent.Laporte@gmail.com>2016-10-31 19:10:39 +0100
committerVincent Laporte <Vincent.Laporte@gmail.com>2016-11-02 19:23:15 +0100
commit5f49eeb935112e69f8992083ca173728a90cbf8c (patch)
treead4d8063be6fe44d76f9a4cdde5a7be3ab1cf016
parent7c53518663658db36218fa8f5566442d3f71da99 (diff)
downloadnixpkgs-5f49eeb935112e69f8992083ca173728a90cbf8c.tar
nixpkgs-5f49eeb935112e69f8992083ca173728a90cbf8c.tar.gz
nixpkgs-5f49eeb935112e69f8992083ca173728a90cbf8c.tar.bz2
nixpkgs-5f49eeb935112e69f8992083ca173728a90cbf8c.tar.lz
nixpkgs-5f49eeb935112e69f8992083ca173728a90cbf8c.tar.xz
nixpkgs-5f49eeb935112e69f8992083ca173728a90cbf8c.tar.zst
nixpkgs-5f49eeb935112e69f8992083ca173728a90cbf8c.zip
coq: move out of ocamlPackages
-rw-r--r--pkgs/top-level/all-packages.nix22
-rw-r--r--pkgs/top-level/ocaml-packages.nix20
2 files changed, 19 insertions, 23 deletions
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 4e0efdfe5a5..3ac37ea3969 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -16470,13 +16470,27 @@ in
 
   aspino = callPackage ../applications/science/logic/aspino {};
 
-  inherit (ocaml-ng.ocamlPackages_4_01_0) coq;
+  coq = callPackage ../applications/science/logic/coq {
+    inherit (ocamlPackages_4_01_0) ocaml findlib lablgtk;
+    camlp5 = ocamlPackages_4_01_0.camlp5_transitional;
+  };
 
-  inherit (ocamlPackages) coq_HEAD;
+  coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
+    inherit (ocamlPackages) ocaml findlib lablgtk;
+    camlp5 = ocamlPackages.camlp5_transitional;
+  };
 
-  inherit (ocamlPackages) coq_8_5;
+  coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
+    inherit (ocamlPackages) ocaml findlib lablgtk;
+    camlp5 = ocamlPackages.camlp5_transitional;
+  };
 
-  inherit (ocaml-ng.ocamlPackages_3_12_1) coq_8_3;
+  coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
+    make = pkgs.gnumake3;
+    inherit (ocamlPackages_3_12_1) ocaml findlib;
+    camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
+    lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
+  };
 
   mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
 
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 58e9512e31c..d4ca17f6dbd 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -612,7 +612,7 @@ let
       then { tools = pkgs.pkgsi686Linux.stdenv.cc; }
       else {}
     ) // {
-      coq = coq_8_5;
+      coq = pkgs.coq_8_5;
     });
 
     haxe = callPackage ../development/compilers/haxe { };
@@ -654,24 +654,6 @@ let
       enableX11 = config.unison.enableX11 or true;
     };
 
-    coq = callPackage ../applications/science/logic/coq {
-      camlp5 = camlp5_transitional;
-    };
-
-    coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
-      camlp5 = camlp5_transitional;
-    };
-
-    coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
-      camlp5 = camlp5_transitional;
-    };
-
-    coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
-      make = pkgs.gnumake3;
-      camlp5 = camlp5_transitional;
-      lablgtk = lablgtk_2_14;
-    };
-
     hol_light = callPackage ../applications/science/logic/hol_light {
       camlp5 = camlp5_strict;
     };