diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/coq-modules/tlc/default.nix
new file mode 100644
index 00000000000..63ad2522ad2
--- /dev/null
+++ b/pkgs/development/coq-modules/tlc/default.nix
@@ -0,0 +1,29 @@
+{stdenv, fetchsvn, coq}:
+
+stdenv.mkDerivation {
+
+  name = "coq-tlc-${coq.coq-version}";
+
+  src = fetchsvn {
+    url = svn://scm.gforge.inria.fr/svn/tlc/branches/v3.1;
+    rev = 240;
+    sha256 = "0mjnb6n9wzb13y2ix9cvd6irzd9d2gj8dcm2x71wgan0jcskxadm";
+  };
+
+  buildInputs = [ coq.ocaml coq.camlp5 ];
+  propagatedBuildInputs = [ coq ];
+
+  installPhase = ''
+    COQLIB=$out/lib/coq/${coq.coq-version}/
+    ensureDir $COQLIB/user-contrib/Tlc
+    cp -p *.vo $COQLIB/user-contrib/Tlc
+  '';
+
+  meta = with stdenv.lib; {
+    homepage = http://www.chargueraud.org/softs/tlc/;
+    description = "TLC is a general purpose Coq library that provides an alternative to Coq's standard library";
+    maintainers = with maintainers; [ jwiegley ];
+    platforms = coq.meta.platforms;
+  };
+
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index c429a1c7b6d..349f6aa1f33 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -11593,6 +11593,8 @@ let
 
     ssreflect = callPackage ../development/coq-modules/ssreflect {};
 
+    tlc = callPackage ../development/coq-modules/tlc {};
+
   };
 
   coqPackages = recurseIntoAttrs (mkCoqPackages_8_4 coqPackages);