diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix
index c554b5dcea1..764954f54f8 100644
--- a/pkgs/applications/science/logic/ssreflect/default.nix
+++ b/pkgs/applications/science/logic/ssreflect/default.nix
@@ -6,7 +6,7 @@
let
pname = "ssreflect";
- version = "1.3pl4";
+ version = "1.4";
name = "${pname}-${version}";
webpage = http://www.msr-inria.inria.fr/Projects/math-components;
in
@@ -15,22 +15,16 @@ stdenv.mkDerivation {
inherit name;
src = fetchurl {
- url = "${webpage}/${name}.tar.gz";
- sha256 = "1ha3iiqq79pgll5ra9z0xdi3d3dr3wb9f5vsm4amy884l5anva02";
+ url = "${webpage}/${name}-coq8.4.tar.gz";
+ sha256 = "1ysx29xw09i86lq0d92z9cnyx133jfgq4qddy3501000fn7xwi7h";
};
buildInputs = [ ocaml camlp5 coq makeWrapper ];
patches = [ ./static.patch ];
- postBuild = ''
- cd src
- coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
- cd ..
- '';
-
installPhase = ''
- COQLIB=$out/lib/coq make -f Makefile.coq install -e
+ COQLIB=$out/lib/coq/ make -f Makefile.coq install -e
mkdir -p $out/bin
cp bin/* $out/bin
for i in $out/bin/*; do
@@ -39,6 +33,7 @@ stdenv.mkDerivation {
--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 = {
diff --git a/pkgs/applications/science/logic/ssreflect/static.patch b/pkgs/applications/science/logic/ssreflect/static.patch
index edb8a6111f7..2211d880258 100644
--- a/pkgs/applications/science/logic/ssreflect/static.patch
+++ b/pkgs/applications/science/logic/ssreflect/static.patch
@@ -1,33 +1,21 @@
---- ssreflect1.3pl4/Make (revision 3823)
-+++ ssreflect1.3pl4/Make (working copy)
-@@ -1,18 +1,18 @@
- ## Uncomment for static linking
- ##
--#
--#-custom "$(COQBIN)coqmktop -opt -o bin/ssrcoq src/ssreflect.cmx" "src/ssreflect.cmx" bin/ssrcoq
--#-custom "$(COQBIN)coqmktop -o bin/ssrcoq.byte src/ssreflect.cmo" "src/ssreflect.cmo bin/ssrcoq" bin/ssrcoq.byte
+--- 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
--#
-+
-+-custom "$(COQBIN)coqmktop -opt -o bin/ssrcoq src/ssreflect.cmx" "src/ssreflect.cmx" bin/ssrcoq
-+-custom "$(COQBIN)coqmktop -o bin/ssrcoq.byte src/ssreflect.cmo" "src/ssreflect.cmo bin/ssrcoq" bin/ssrcoq.byte
+-##
++## 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 dynamic linking
- ##
--
---I src
--
+#
-+#-I src
-+#
- ##
## What follows should be left untouched by the final user of ssreflect
-Common subdirectories: old/src and new/src
-Common subdirectories: old/test and new/test
-Common subdirectories: old/theories and new/theories
+ -R theories Ssreflect
+
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 88cfccf24a3..74edde7615d 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -8575,7 +8575,6 @@ let
spass = callPackage ../applications/science/logic/spass {};
ssreflect = callPackage ../applications/science/logic/ssreflect {
- coq = coq_8_3;
camlp5 = ocamlPackages.camlp5_transitional;
};