diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 3fef10b44fb2..cfd769fa6a2c 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -4,7 +4,7 @@
 {stdenv, fetchurl, ocaml, findlib, camlp5, lablgtk, ncurses}:
 
 let
-  version = "8.3pl3";
+  version = "8.3pl4";
 in
 
 stdenv.mkDerivation {
@@ -12,7 +12,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "http://coq.inria.fr/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "0ivrafwr4p8pklb9wfq3zyai19xdk05xr3q16xqk4q9pfad9w9dg";
+    sha256 = "17d3lmchmqir1rawnr52g78srg4wkd7clzpzfsivxc4y1zp6rwkr";
   };
 
   buildInputs = [ ocaml findlib camlp5 ncurses lablgtk ];
@@ -58,5 +58,6 @@ stdenv.mkDerivation {
     '';
     homepage = "http://coq.inria.fr";
     license = "LGPL";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
   };
 }
diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix
index 8443974a0a0a..c554b5dcea1c 100644
--- a/pkgs/applications/science/logic/ssreflect/default.nix
+++ b/pkgs/applications/science/logic/ssreflect/default.nix
@@ -2,11 +2,11 @@
 # - 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}:
+{stdenv, fetchurl, ocaml, camlp5, coq, makeWrapper}:
 
 let
   pname = "ssreflect";
-  version = "1.3pl1";
+  version = "1.3pl4";
   name = "${pname}-${version}";
   webpage = http://www.msr-inria.inria.fr/Projects/math-components;
 in
@@ -16,22 +16,29 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "${webpage}/${name}.tar.gz";
-    sha256 = "0ykrhqb68aanl5d4dmn0vnx8m34gg0jsbdhwx2852rqi7r00b9ri";
+    sha256 = "1ha3iiqq79pgll5ra9z0xdi3d3dr3wb9f5vsm4amy884l5anva02";
   };
 
-  buildInputs = [ ocaml camlp5 coq ];
+  buildInputs = [ ocaml camlp5 coq makeWrapper ];
+
+  patches = [ ./static.patch ];
 
-  # this fails
-  /*
   postBuild = ''
     cd src
     coqmktop -ide -opt ssreflect.cmx -o ../bin/ssrcoqide
+    cd ..
   '';
-  */
 
   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
   '';
 
   meta = {
@@ -43,5 +50,6 @@ stdenv.mkDerivation {
     '';
     homepage = webpage;
     license = "CeCILL B FREE SOFTWARE LICENSE or CeCILL FREE SOFTWARE LICENSE";
+    maintainers = [ stdenv.lib.maintainers.roconnor ];
   };
 }
diff --git a/pkgs/applications/science/logic/ssreflect/static.patch b/pkgs/applications/science/logic/ssreflect/static.patch
new file mode 100644
index 000000000000..edb8a6111f7e
--- /dev/null
+++ b/pkgs/applications/science/logic/ssreflect/static.patch
@@ -0,0 +1,33 @@
+--- ssreflect1.3pl4/Make	(revision 3823)
++++ ssreflect1.3pl4/Make	(working copy)
+@@ -1,18 +1,18 @@
+ ## Uncomment for static linking
+ ## <static>
+-#
+-#-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
+-#-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
++-custom "$(SSRCOQ) $(COQFLAGS) -compile $*" "%.v $(SSRCOQ)" "%.vo"
++SSRCOQ = bin/ssrcoq
++
+ ## </static>
+ 
+ ## Uncomment for dynamic linking
+ ## <dynamic>
+-
+--I src
+-
++#
++#-I src
++#
+ ## </dynamic>
+ 
+ ## 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