diff --git a/nix/alt-ergo.nix b/nix/alt-ergo.nix
index 159534d5d6aa17a3e61d07fd862648c0d537607f..75288b5ff80bfb9a250f48bf2fd1964af1188222 100644
--- a/nix/alt-ergo.nix
+++ b/nix/alt-ergo.nix
@@ -1,50 +1,47 @@
-{ callPackage
-, fetchzip
-, lib
-, stdenv
-, ocaml
-, findlib
-, ocplib-simplex
-, psmt2-frontend
-, lablgtk
-, zarith
-, menhir
-, camlzip
-, num
-, which
-, autoreconfHook
-}:
-
-stdenv.mkDerivation rec {
-  pname = "alt-ergo";
-  version = "2.2.0-free";
-
-  src = fetchzip {
-    url = https://alt-ergo.ocamlpro.com/http/alt-ergo-free-2.2.0/alt-ergo-free-2.2.0.tar.gz;
-    sha256 = "11ffm87vsrii8nyhxhbc9gzjmqkspqv7hpjq7ll9xflll7gpnpkj";
-    stripRoot=false;
-  };
-
-  nativeBuildInputs = [
-    autoreconfHook
-    which
-  ];
+{ fetchFromGitHub, fetchpatch, lib, which, ocamlPackages }:
 
-  buildInputs = [
-    ocaml
-    findlib
-    zarith
-    ocplib-simplex
-    psmt2-frontend
-    lablgtk
-    menhir
-  ];
-
-  propagatedBuildInputs = [ camlzip num ];
+let
+  pname = "alt-ergo";
+  version = "2.4.2";
 
-  enableParallelBuilding = true;
+  configureScript = "ocaml unix.cma configure.ml";
 
-  configureFlags = [ "--enable-verbose-make" ];
+  src = fetchFromGitHub {
+    owner = "OCamlPro";
+    repo = pname;
+    rev = "refs/tags/${version}";
+    hash = "sha256-8pJ/1UAbheQaLFs5Uubmmf5D0oFJiPxF6e2WTZgRyAc=";
+  };
+in
+
+let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-lib";
+  inherit version src configureScript;
+  configureFlags = [ pname ];
+  nativeBuildInputs = [ which ];
+  buildInputs = with ocamlPackages; [ dune-configurator ];
+  propagatedBuildInputs = with ocamlPackages; [ num ocplib-simplex seq stdlib-shims zarith ];
+  preBuild = ''
+    substituteInPlace src/lib/util/version.ml --replace 'version="dev"' 'version="${version}"'
+  '';
+}; in
+
+let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-parsers";
+  inherit version src configureScript;
+  configureFlags = [ pname ];
+  nativeBuildInputs = [ which ocamlPackages.menhir ];
+  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
+}; in
+
+ocamlPackages.buildDunePackage {
+
+  inherit pname version src configureScript;
+
+  configureFlags = [ pname ];
+
+  nativeBuildInputs = [ which ocamlPackages.menhir ];
+  buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ];
 
   meta = {
     description = "High-performance theorem prover and SMT solver";
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 6127043519682e422e54d413e74084c3a6c2b1c2..6873f8f80140532364ee057865d6e64a5af309de 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -5,9 +5,7 @@ let
     alt-ergo = oself.callPackage ./alt-ergo.nix {};
     camlp5 = oself.callPackage ./camlp5.nix {};
     headache = oself.callPackage ./headache.nix {};
-    menhirLib = oself.callPackage ./menhirLib.nix {};
     mlmpfr = oself.callPackage ./mlmpfr.nix {};
-    psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
     why3 = oself.callPackage ./why3.nix {};
 
     # Helpers
diff --git a/nix/psmt2-frontend.nix b/nix/psmt2-frontend.nix
deleted file mode 100644
index 98836906d462ecce7f597e8e99df178b5c97fbe4..0000000000000000000000000000000000000000
--- a/nix/psmt2-frontend.nix
+++ /dev/null
@@ -1,48 +0,0 @@
-{ callPackage
-, fetchFromGitHub
-, lib
-, stdenv
-, ocaml
-, findlib
-, menhir
-, autoreconfHook
-, which
-}:
-
-stdenv.mkDerivation rec {
-  pname = "psmt2-frontend";
-  version = "0.1";
-
-  src = fetchFromGitHub {
-    owner = "Coquera";
-    repo = pname;
-    rev = version;
-    sha256 = "0k7jlsbkdyg7hafmvynp0ik8xk7mfr00wz27vxn4ncnmp20yz4vn";
-  };
-
-  nativeBuildInputs = [
-    autoreconfHook
-    which
-  ];
-
-  buildInputs = [
-    ocaml
-    findlib
-    menhir
-  ];
-
-  enableParallelBuilding = true;
-
-  configureFlags = [ "--enable-verbose-make" ];
-
-  createFindlibDestdir = true;
-
-  installFlags = "LIBDIR=$(OCAMLFIND_DESTDIR)";
-
-  meta = {
-    description = "A simple parser and type-checker for polomorphic extension of the SMT-LIB 2 language";
-    license = lib.licenses.asl20;
-    maintainers = [ lib.maintainers.vbgl ];
-    inherit (src.meta) homepage;
-  };
-}