diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/coq-modules/smtcoq/default.nix
index a3aeba4881ea..ced7a87640ee 100644
--- a/pkgs/development/coq-modules/smtcoq/default.nix
+++ b/pkgs/development/coq-modules/smtcoq/default.nix
@@ -6,6 +6,7 @@
   zchaff,
   cvc5,
   stdlib,
+  trakt,
   version ? null,
 }:
 
@@ -21,59 +22,72 @@
 #   };
 # in
 
-mkCoqDerivation {
-  pname = "smtcoq";
-  owner = "smtcoq";
+let
+  derivation = mkCoqDerivation {
+    pname = "smtcoq";
+    owner = "smtcoq";
+    opam-name = "rocq-smtcoq";
 
-  release."SMTCoq-2.3+8.20".hash = "sha256-ScWtdwSpFBf/PryPuvI/SkhgqWyYhcX3FCOqoXNho7Q=";
-  release."SMTCoq-2.2+8.19".hash = "sha256-9Wv8AXRRyOHG/cjA/V9tSK55R/bofDMLTkDpuwYWkks=";
-  release."SMTCoq-2.2+8.18".hash = "sha256-1iJAruI5Qn9nTZcUDjk8t/1Q+eFkYLOe9Ee0DmK03w8=";
-  release."SMTCoq-2.2+8.17".hash = "sha256-kaodsyVUl1+QQagzoBTIjxbdD4X3IaaH0x2AsVUL+Z0=";
-  release."SMTCoq-2.2+8.16".hash = "sha256-Hwm8IFlw97YiOY6H63HyJlwIXvQHr9lqc1+PgTnBtkw=";
-  release."SMTCoq-2.2+8.15".hash = "sha256-+GYOasJ32KJyOfqJlTtFmsJ2exd6gdueKwHdeMPErTo=";
-  release."SMTCoq-2.2+8.14".hash = "sha256-jqnF33E/4CqR1HSrLmUmLVCKslw9h3bbWi4YFmFYrhY=";
-  release."SMTCoq-2.2+8.13".hash = "sha256-AVpKU/SLaLYnCnx6GOEPGJjwbRrp28Fs5O50kJqdclI=";
-  release."SMTCoq-2.1+8.16".rev = "4996c00b455bfe98400e96c954839ceea93efdf7";
-  release."SMTCoq-2.1+8.16".hash = "sha256-k53e+frUjwq+ZZKbbOKd/EfVC40QeAzB2nCsGkCKnHA=";
-  release."SMTCoq-2.1+8.14".rev = "e11d9b424b0113f32265bcef0ddc962361da4dae";
-  release."SMTCoq-2.1+8.14".hash = "sha256-4a01/CRHUon2OfpagAnMaEVkBFipPX3MCVmSFS1Bnt4=";
-  release."SMTCoq-2.1+8.13".rev = "d02269c43739f4559d83873563ca00daad9faaf1";
-  release."SMTCoq-2.1+8.13".hash = "sha256-VZetGghdr5uJWDwZWSlhYScoNEoRHIbwqwJKSQyfKKg=";
+    release."SMTCoq-2.3+8.20".hash = "sha256-ScWtdwSpFBf/PryPuvI/SkhgqWyYhcX3FCOqoXNho7Q=";
+    release."SMTCoq-2.2+8.19".hash = "sha256-9Wv8AXRRyOHG/cjA/V9tSK55R/bofDMLTkDpuwYWkks=";
+    release."SMTCoq-2.2+8.18".hash = "sha256-1iJAruI5Qn9nTZcUDjk8t/1Q+eFkYLOe9Ee0DmK03w8=";
+    release."SMTCoq-2.2+8.17".hash = "sha256-kaodsyVUl1+QQagzoBTIjxbdD4X3IaaH0x2AsVUL+Z0=";
+    release."SMTCoq-2.2+8.16".hash = "sha256-Hwm8IFlw97YiOY6H63HyJlwIXvQHr9lqc1+PgTnBtkw=";
+    release."SMTCoq-2.2+8.15".hash = "sha256-+GYOasJ32KJyOfqJlTtFmsJ2exd6gdueKwHdeMPErTo=";
+    release."SMTCoq-2.2+8.14".hash = "sha256-jqnF33E/4CqR1HSrLmUmLVCKslw9h3bbWi4YFmFYrhY=";
+    release."SMTCoq-2.2+8.13".hash = "sha256-AVpKU/SLaLYnCnx6GOEPGJjwbRrp28Fs5O50kJqdclI=";
+    release."SMTCoq-2.1+8.16".rev = "4996c00b455bfe98400e96c954839ceea93efdf7";
+    release."SMTCoq-2.1+8.16".hash = "sha256-k53e+frUjwq+ZZKbbOKd/EfVC40QeAzB2nCsGkCKnHA=";
+    release."SMTCoq-2.1+8.14".rev = "e11d9b424b0113f32265bcef0ddc962361da4dae";
+    release."SMTCoq-2.1+8.14".hash = "sha256-4a01/CRHUon2OfpagAnMaEVkBFipPX3MCVmSFS1Bnt4=";
+    release."SMTCoq-2.1+8.13".rev = "d02269c43739f4559d83873563ca00daad9faaf1";
+    release."SMTCoq-2.1+8.13".hash = "sha256-VZetGghdr5uJWDwZWSlhYScoNEoRHIbwqwJKSQyfKKg=";
 
-  releaseRev = v: v;
+    releaseRev = v: v;
 
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch coq.coq-version [
-      (case (isEq "8.20") "SMTCoq-2.3+${coq.coq-version}")
-      (case (range "8.13" "8.19") "SMTCoq-2.2+${coq.coq-version}")
-    ] null;
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      with lib.versions;
+      lib.switch coq.coq-version [
+        (case (isEq "8.20") "SMTCoq-2.3+${coq.coq-version}")
+        (case (range "8.13" "8.19") "SMTCoq-2.2+${coq.coq-version}")
+      ] null;
 
-  propagatedBuildInputs = [
-    cvc5
-    # veriT'  # c.f. comment above
-    zchaff
-    stdlib
-  ]
-  ++ (with coq.ocamlPackages; [
-    findlib
-    num
-    zarith
-  ]);
-  mlPlugin = true;
-  nativeBuildInputs = (with pkgs; [ gnumake42 ]) ++ (with coq.ocamlPackages; [ ocamlbuild ]);
+    propagatedBuildInputs = [
+      cvc5
+      # veriT'  # c.f. comment above
+      zchaff
+      stdlib
+    ]
+    ++ (with coq.ocamlPackages; [
+      findlib
+      num
+      zarith
+    ]);
+    useDuneifVersion = v: v != null && (v == "dev" || lib.versions.isGt "SMTCoq-2.3+8.20" v);
+    mlPlugin = true;
+    nativeBuildInputs = (with pkgs; [ gnumake42 ]) ++ (with coq.ocamlPackages; [ ocamlbuild ]);
 
-  # This is meant to ease future troubleshooting of cvc5 build failures
-  passthru = { inherit cvc5; };
+    # This is meant to ease future troubleshooting of cvc5 build failures
+    passthru = { inherit cvc5; };
 
-  meta = {
-    description = "Communication between Coq and SAT/SMT solvers";
-    maintainers = with lib.maintainers; [ siraben ];
-    license = lib.licenses.cecill-b;
-    platforms = lib.platforms.unix;
+    meta = {
+      description = "Communication between Coq and SAT/SMT solvers";
+      maintainers = with lib.maintainers; [ siraben ];
+      license = lib.licenses.cecill-b;
+      platforms = lib.platforms.unix;
+    };
   };
-}
+  patched-derivation1 = derivation.overrideAttrs (
+    o:
+    lib.optionalAttrs
+      (o.version != null && (o.version == "dev" || lib.versions.isGt "SMTCoq-2.3+8.20" o.version))
+      {
+        propagatedBuildInputs = o.propagatedBuildInputs ++ [ trakt ];
+      }
+  );
+in
+patched-derivation1