Removes duplicate ssreflect

pkgs/applications/science/logic/ssreflect/default.nix

@@ -1,50 +0,0 @@
-# TODO:
-# - coq needs to be invoked with the explicit path to the ssreflect theory
-#   e.g. coqide -R ~/.nix-profile/lib/coq/user-contrib/ ''
-
-{stdenv, fetchurl, ocaml, camlp5, coq, makeWrapper}:
-
-let
-  pname = "ssreflect";
-  version = "1.5";
-  name = "${pname}-${version}";
-  webpage = http://www.msr-inria.inria.fr/Projects/math-components;
-in
-
-stdenv.mkDerivation {
-  inherit name;
-
-  src = fetchurl {
-    url = "http://ssr.msr-inria.inria.fr/FTP/${name}.tar.gz";
-    sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
-  };
-
-  buildInputs = [ ocaml camlp5 coq makeWrapper ];
-
-  patches = [ ./static.patch ];
-
-  installPhase = ''
-    COQLIB=$out/lib/coq/ make -f Makefile.coq install -e
-    mkdir -p $out/bin
-    cp bin/* $out/bin
-    for i in $out/bin/*; do
-      wrapProgram "$i" \
-        --add-flags "-R" \
-        --add-flags "$out/lib/coq/user-contrib/Ssreflect" \
-        --add-flags "Ssreflect"
-    done
-    makeWrapper "${coq}/bin/coqide" "$out/bin/ssrcoqide" --add-flags "-coqtop" --add-flags "$out/bin/ssrcoq"
-  '';
-
-  meta = {
-    description = "Small Scale Reflection extension for Coq";
-    longDescription = ''
-      Small Scale Reflection (ssreflect) is an extension of the Coq Theorem
-      Prover which enable a formal proof methodology based on the pervasive
-      use of computation with symbolic representation
-    '';
-    homepage = webpage;
-    license = "CeCILL B FREE SOFTWARE LICENSE or CeCILL FREE SOFTWARE LICENSE";
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
-  };
-}

pkgs/applications/science/logic/ssreflect/static.patch

@@ -1,21 +0,0 @@
---- ssreflect1.4-coq8.4/Make	(revision 3823)
-+++ ssreflect1.4-coq8.4/Make	(working copy)
-@@ -1,10 +1,10 @@
--### Uncomment for static linking
--##
--#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
--#-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
--#-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
--#SSRCOQ = bin/ssrcoq
--##
-+## Uncomment for static linking
-+#
-+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -opt -o bin/ssrcoq src/ssrmatching.cmx src/ssreflect.cmx" "src/ssrmatching.cmx src/ssreflect.cmx" bin/ssrcoq
-+-custom "$(COQBIN)coqmktop -coqlib `$(COQBIN)coqtop -where` -o bin/ssrcoq.byte src/ssrmatching.cmo src/ssreflect.cmo" "src/ssrmatching.cmo src/ssreflect.cmo" bin/ssrcoq.byte
-+-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
-+SSRCOQ = bin/ssrcoq
-+#
- 
- ## What follows should be left untouched by the final user of ssreflect
- -R theories Ssreflect
-

pkgs/top-level/all-packages.nix

@@ -11519,10 +11519,6 @@ let
 
   spass = callPackage ../applications/science/logic/spass {};
 
-  ssreflect = callPackage ../applications/science/logic/ssreflect {
-    camlp5 = ocamlPackages.camlp5_transitional;
-  };
-
   tptp = callPackage ../applications/science/logic/tptp {};
 
   twelf = callPackage ../applications/science/logic/twelf {