diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix
new file mode 100644
index 000000000000..b76dd1b43d12
--- /dev/null
+++ b/pkgs/development/coq-modules/gappalib/default.nix
@@ -0,0 +1,30 @@
+{ stdenv, fetchurl, which, coq, flocq }:
+
+stdenv.mkDerivation {
+  name = "coq${coq.coq-version}-gappalib-1.4.1";
+  src = fetchurl {
+    url = https://gforge.inria.fr/frs/download.php/file/37917/gappalib-coq-1.4.1.tar.gz;
+    sha256 = "0d3f23a871haglg8hq1jgxz3y5nryiwy12b5xfnfjn279jfqqjw4";
+  };
+
+  nativeBuildInputs = [ which ];
+  buildInputs = [ coq coq.ocamlPackages.ocaml ];
+  propagatedBuildInputs = [ flocq ];
+
+  configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Gappa";
+  buildPhase = "./remake";
+  installPhase = "./remake install";
+
+  meta = {
+    description = "Coq support library for Gappa";
+    license = stdenv.lib.licenses.lgpl21;
+    homepage = http://gappa.gforge.inria.fr/;
+    maintainers = [ stdenv.lib.maintainers.vbgl ];
+    inherit (coq.meta) platforms;
+  };
+
+  passthru = {
+    compatibleCoqVersions = stdenv.lib.flip stdenv.lib.versionAtLeast "8.7";
+  };
+
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 725ea6db2dea..524f3bf43994 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -27,6 +27,7 @@ let
       equations = callPackage ../development/coq-modules/equations { };
       fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
       flocq = callPackage ../development/coq-modules/flocq {};
+      gappalib = callPackage ../development/coq-modules/gappalib {};
       heq = callPackage ../development/coq-modules/heq {};
       HoTT = callPackage ../development/coq-modules/HoTT {};
       interval = callPackage ../development/coq-modules/interval {};