diff --git a/.github/labeler.yml b/.github/labeler.yml
index 524bfea1a1b3..51a10a54daac 100644
--- a/.github/labeler.yml
+++ b/.github/labeler.yml
@@ -43,14 +43,6 @@
               - .github/**/*
               - ci/**/*.*
 
-"6.topic: coq":
-  - any:
-      - changed-files:
-          - any-glob-to-any-file:
-              - pkgs/applications/science/logic/coq/**/*
-              - pkgs/development/coq-modules/**/*
-              - pkgs/top-level/coq-packages.nix
-
 "6.topic: COSMIC":
   - any:
       - changed-files:
@@ -466,6 +458,18 @@
           - any-glob-to-any-file:
               - pkgs/development/rocm-modules/**/*
 
+"6.topic: rocq":
+  - any:
+      - changed-files:
+          - any-glob-to-any-file:
+              - pkgs/applications/science/logic/coq/**/*
+              - pkgs/applications/science/logic/rocq-core/**/*
+              - pkgs/build-support/coq/**/*
+              - pkgs/build-support/rocq/**/*
+              - pkgs/development/rocq-modules/**/*
+              - pkgs/top-level/coq-packages.nix
+              - pkgs/top-level/rocq-packages.nix
+
 "6.topic: ruby":
   - any:
       - changed-files:
diff --git a/doc/languages-frameworks/rocq.section.md b/doc/languages-frameworks/rocq.section.md
index 6aec9e804c26..ebdda5bb617b 100644
--- a/doc/languages-frameworks/rocq.section.md
+++ b/doc/languages-frameworks/rocq.section.md
@@ -3,11 +3,12 @@
 Note that "The Rocq Prover" (Rocq for short) is the new name of the
 proof assistant formerly known as Coq. The `coq` and `coqPackages`
 derivations currently remain for both older versions of Coq, but also
-some versions of Rocq during the renaming transition. In the latter
-case, the `coq` derivation encompasses the compatibility binaries
-(`coqtop`, `coqc`, etc.) in addition to the `rocq` binary. The packages
-only in `coqPackages` are the ones which currently still depend on these
-compatibility binaries.
+as compatibility aliases for some versions of Rocq. In both cases, the
+`coq` and `rocq-core` attributes exist. In the case of Coq (< 9),
+`rocq-core` is just an alias for `coq`, while in the case of Rocq (>= 9),
+`rocq-core` is the main Rocq derivation, while `coq` provides
+compatibility binaries (`coqc`, `coqtop`, etc.) for packages that still
+depend on them.
 
 ## Rocq derivation: `rocq-core` {#rocq-derivation-rocq}
 
@@ -17,18 +18,18 @@ The Rocq derivation is overridable through the `rocq-core.override overrides`, w
 * `customOCamlPackages` (optional, defaults to `null`, which lets Rocq choose a version automatically), which can be set to any of the ocaml packages attribute of `ocaml-ng` (such as `ocaml-ng.ocamlPackages_4_14` which is the default for Rocq 9.1 for example).
 * `rocq-version` (optional, defaults to the short version e.g. "9.1"), is a version number of the form "x.y" that indicates which Rocq's version build behavior to mimic when using a source which is not a release. E.g. `rocq-core.override { version = "40be8435e132aab2231a79091f011ebc3e64a753"; rocq-version = "9.1"; }`.
 
-## Creating custom Coq environments with `coq.withPackages` {#coq-withPackages}
+## Creating custom Coq environments with `rocq-core.withPackages` {#coq-withPackages}
 
-The `coq.withPackages` function provides a convenient way to create a Coq environment that includes additional Coq packages. This is similar to how `python.withPackages` works for Python environments.
+The `rocq-core.withPackages` function provides a convenient way to create a Rocq environment that includes additional Rocq packages. This is similar to how `python.withPackages` works for Python environments.
 
-The function takes a function that receives the Coq package set and returns a list of packages. It returns a wrapped Coq environment where all Coq binaries (`coqtop`, `coqc`, `coqdep`, `coqchk`, `coqide`, etc.) are configured with the appropriate environment variables to find the packages.
+The function takes a function that receives the Rocq package set and returns a list of packages. It returns a wrapped Rocq environment where the Rocq binaries (`rocq`, etc.) are configured with the appropriate environment variables to find the packages.
 
 ### Usage {#coq-withPackages-usage}
 
-Here is an example of creating a Coq environment with specific packages.
+Here is an example of creating a Rocq environment with specific packages.
 
 ```nix
-coq.withPackages (
+rocq-core.withPackages (
   ps: with ps; [
     mathcomp
     bignums
@@ -36,7 +37,9 @@ coq.withPackages (
 )
 ```
 
-If you install the `vsrocq-language-server` or `rocq-lsp` server, make sure to list them as part of the above `coq.withPackages` expression instead of installing them separately if you want them to find your Coq/Rocq packages.
+If you install the `vsrocq-language-server` or `rocq-lsp` server, make sure to list them as part of the above `rocq-core.withPackages` expression instead of installing them separately if you want them to find your Rocq packages.
+
+For versions prior to Rocq 9.0, a similar `coq.withPackages` function is available.
 
 ## Rocq packages attribute sets: `rocqPackages` {#rocq-packages-attribute-sets-rocqpackages}
 
@@ -130,7 +133,7 @@ mkRocqDerivation {
     mathcomp.boot
     mathcomp.algebra
     mathcomp-finmap
-    mathcomp.fingroup
+    mathcomp.finite-group
     mathcomp-bigenough
   ];
 
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 39c8278a232e..70326bbdf59e 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -100,6 +100,7 @@ let
   version = fetched.version;
   coq-version =
     args.coq-version or (if version != "dev" then lib.versions.majorMinor version else "dev");
+  rocq-version = coq-version;
   coqAtLeast = v: coq-version == "dev" || lib.versionAtLeast coq-version v;
   buildIde = args.buildIde or (coqAtLeast "8.10" && !coqAtLeast "8.14");
   csdpPatch = lib.optionalString (csdp != null) ''
@@ -161,6 +162,7 @@ let
 
     passthru = {
       inherit coq-version;
+      inherit rocq-version;
       inherit ocamlPackages ocamlNativeBuildInputs;
       inherit ocamlPropagatedBuildInputs;
       # For compatibility
diff --git a/pkgs/applications/science/logic/coq/with-packages.nix b/pkgs/applications/science/logic/coq/with-packages.nix
index 62a95c927f84..64a85328b15a 100644
--- a/pkgs/applications/science/logic/coq/with-packages.nix
+++ b/pkgs/applications/science/logic/coq/with-packages.nix
@@ -11,7 +11,8 @@ packages:
 let
   # At version 9.0, Coq underwent a name change to Rocq.
   # A couple paths and environment variables need to change at this point.
-  isRocq = lib.versionAtLeast coq.coq-version "9.0";
+  isRocq = coq ? rocq-version && lib.versionAtLeast coq.rocq-version "9.0";
+  rocq-version = if isRocq then coq.rocq-version else coq.coq-version;
 
   collectPropagated =
     pkg:
@@ -21,9 +22,9 @@ let
 
   allPackages = lib.unique (lib.concatMap collectPropagated packages);
 
-  coqPath = lib.makeSearchPath "/lib/coq/${coq.coq-version}/user-contrib" allPackages;
+  coqPath = lib.makeSearchPath "/lib/coq/${rocq-version}/user-contrib" allPackages;
 
-  ocamlPath = lib.makeSearchPath "/lib/ocaml/${coq.ocaml.version}/site-lib" (
+  ocamlPath = lib.makeSearchPath "/lib/ocaml/${coq.ocamlPackages.ocaml.version}/site-lib" (
     [ coq.ocamlPackages.findlib ] ++ allPackages
   );
 
diff --git a/pkgs/build-support/rocq/default.nix b/pkgs/build-support/rocq/default.nix
index 6a25a171cb25..996acbed09e7 100644
--- a/pkgs/build-support/rocq/default.nix
+++ b/pkgs/build-support/rocq/default.nix
@@ -213,6 +213,12 @@ stdenv.mkDerivation (
         }
         // (args.env or { });
 
+      preBuild =
+        optionalString (useCoq && useDune && lib.versionAtLeast rocq-core.rocq-version "9.0") ''
+          export COQPATH="$ROCQPATH"
+        ''
+        + (args.preBuild or "");
+
       meta =
         (
           {
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
deleted file mode 100644
index d3548a970560..000000000000
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ /dev/null
@@ -1,63 +0,0 @@
-{
-  lib,
-  mkCoqDerivation,
-  coq,
-  stdlib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-    pname = "bignums";
-    owner = "rocq-community";
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (range "8.13" "8.20") "9.0.0+coq${coq.coq-version}")
-        (case (range "8.6" "8.17") "${coq.coq-version}.0")
-      ] null;
-
-    release."9.0.0+coq8.20".hash = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";
-    release."9.0.0+coq8.19".hash = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ=";
-    release."9.0.0+coq8.18".hash = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8=";
-    release."9.0.0+coq8.17".hash = "sha256-Mn85LqxJKPDIfpxRef9Uh5POwOKlTQ7jsMVz1wnQwuY=";
-    release."9.0.0+coq8.16".hash = "sha256-pwFTl4Unr2ZIirAB3HTtfhL2YN7G/Pg88RX9AhKWXbE=";
-    release."9.0.0+coq8.15".hash = "sha256-2oGOANn3XULHNIlyqjZ5ppQTQa2QF1zzf3YjHAd/pjo=";
-    release."9.0.0+coq8.14".hash = "sha256-qTU152Dz34W6nFZ0pPbja9ouUm/714ZrLQ/Z4N/HIC4=";
-    release."9.0.0+coq8.13".hash = "sha256-zvAqV3VAB7cN+nlMhjSXzxuDkdd387ju2VSb2EUthI0=";
-    release."8.17.0".hash = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
-    release."8.16.0".hash = "sha256-DH3iWwatPlhhCVYVlgL2WLkvneSVzSXUiKo2e0+1zR4=";
-    release."8.15.0".hash = "sha256:093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";
-    release."8.14.0".hash = "sha256:0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06";
-    release."8.13.0".hash = "sha256:1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
-    release."8.12.0".hash = "sha256:14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
-    release."8.11.0".hash = "sha256:1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
-    release."8.10.0".hash = "sha256:0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
-    release."8.9.0".hash = "sha256:03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
-    release."8.8.0".hash = "sha256:1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
-    release."8.7.0".hash = "sha256:11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
-    release."8.6.0".rev = "v8.6.0";
-    release."8.6.0".hash = "sha256:0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
-    releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}";
-
-    mlPlugin = true;
-
-    propagatedBuildInputs = [ stdlib ];
-
-    meta = {
-      license = lib.licenses.lgpl2;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.bignums for Rocq >= 9.0
-if coq.rocqPackages ? bignums then
-  coq.rocqPackages.bignums.override {
-    inherit version stdlib;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
deleted file mode 100644
index b8af7bbf4664..000000000000
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ /dev/null
@@ -1,84 +0,0 @@
-{
-  lib,
-  mkCoqDerivation,
-  coq,
-  stdlib,
-  coq-elpi,
-  version ? null,
-}:
-
-let
-  hb = mkCoqDerivation {
-    pname = "hierarchy-builder";
-    owner = "math-comp";
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (range "8.20" "8.20") "1.9.1")
-        (case (range "8.19" "8.20") "1.8.0")
-        (case (range "8.18" "8.20") "1.7.1")
-        (case (range "8.16" "8.18") "1.6.0")
-        (case (range "8.15" "8.18") "1.5.0")
-        (case (range "8.15" "8.17") "1.4.0")
-        (case (range "8.13" "8.14") "1.2.0")
-        (case (range "8.12" "8.13") "1.1.0")
-        (case (isEq "8.11") "0.10.0")
-      ] null;
-    release."1.9.1".hash = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
-    release."1.8.1".hash = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4=";
-    release."1.8.0".hash = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
-    release."1.7.1".hash = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
-    release."1.7.0".hash = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
-    release."1.6.0".hash = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg=";
-    release."1.5.0".hash = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c=";
-    release."1.4.0".hash = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw=";
-    release."1.3.0".hash = "sha256:17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc";
-    release."1.2.1".hash = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
-    release."1.2.0".hash = "sha256:0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
-    release."1.1.0".hash = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
-    release."1.0.0".hash = "sha256:0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
-    release."0.10.0".hash = "sha256:1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
-    releaseRev = v: "v${v}";
-
-    propagatedBuildInputs = [ coq-elpi ];
-
-    mlPlugin = true;
-
-    meta = {
-      description = "High level commands to declare a hierarchy based on packed classes";
-      maintainers = with lib.maintainers; [
-        cohencyril
-        siraben
-      ];
-      license = lib.licenses.mit;
-    };
-  };
-  hb2 = hb.overrideAttrs (
-    o:
-    lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {
-      buildPhase = "make build";
-    }
-    // (
-      if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then
-        { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
-      else
-        { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }
-    )
-    // lib.optionalAttrs (o.version != null && o.version == "1.8.1") {
-      propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
-    }
-  );
-in
-# this is just a wrapper for rocqPackages.hierarchy-builder for Rocq >= 9.0
-if coq.rocqPackages ? hierarchy-builder then
-  coq.rocqPackages.hierarchy-builder.override {
-    inherit version;
-    inherit (coq.rocqPackages) rocq-core;
-    rocq-elpi = coq-elpi;
-  }
-else
-  hb2
diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix
deleted file mode 100644
index faa48096f836..000000000000
--- a/pkgs/development/coq-modules/iris/default.nix
+++ /dev/null
@@ -1,65 +0,0 @@
-{
-  lib,
-  mkCoqDerivation,
-  coq,
-  stdpp,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-    pname = "iris";
-    domain = "gitlab.mpi-sws.org";
-    owner = "iris";
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (range "8.19" "9.1") "4.4.0")
-        (case (range "8.18" "8.19") "4.2.0")
-        (case (range "8.16" "8.18") "4.1.0")
-        (case (range "8.13" "8.17") "4.0.0")
-        (case (range "8.12" "8.14") "3.5.0")
-        (case (range "8.11" "8.13") "3.4.0")
-        (case (range "8.9" "8.10") "3.3.0")
-      ] null;
-    release."4.4.0".hash = "sha256-zpuaIdH2ScOuZB0Vt1TEHAbsmcT1DyoDsJpftT1M7qw=";
-    release."4.3.0".hash = "sha256-3qhjiFI+A3I3fD8rFfJL5Hek77wScfn/FNNbDyGqA1k=";
-    release."4.2.0".hash = "sha256-HuiHIe+5letgr1NN1biZZFq0qlWUbFmoVI7Q91+UIfM=";
-    release."4.1.0".hash = "sha256-nTZUeZOXiH7HsfGbMKDE7vGrNVCkbMaWxdMWUcTUNlo=";
-    release."4.0.0".hash = "sha256-Jc9TmgGvkiDaz9IOoExyeryU1E+Q37GN24NIM397/Gg=";
-    release."3.6.0".hash = "sha256:02vbq597fjxd5znzxdb54wfp36412wz2d4yash4q8yddgl1kakmj";
-    release."3.5.0".hash = "sha256:0hh14m0anfcv65rxm982ps2vp95vk9fwrpv4br8bxd9vz0091d70";
-    release."3.4.0".hash = "sha256:0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb";
-    release."3.3.0".hash = "sha256:0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
-    releaseRev = v: "iris-${v}";
-
-    propagatedBuildInputs = [ stdpp ];
-
-    preBuild = ''
-      if [[ -f coq-lint.sh ]]
-      then patchShebangs coq-lint.sh
-      fi
-    '';
-
-    meta = {
-      description = "Coq development of the Iris Project";
-      license = lib.licenses.bsd3;
-      maintainers = [
-        lib.maintainers.vbgl
-        lib.maintainers.ineol
-      ];
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.iris for Rocq >= 9.0
-if coq.rocqPackages ? iris then
-  coq.rocqPackages.iris.override {
-    inherit version stdpp;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
deleted file mode 100644
index eb2363285f49..000000000000
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ /dev/null
@@ -1,255 +0,0 @@
-{
-  lib,
-  mkCoqDerivation,
-  mathcomp,
-  mathcomp-finmap,
-  mathcomp-bigenough,
-  hierarchy-builder,
-  stdlib,
-  single ? false,
-  coq,
-  version ? null,
-}@args:
-
-let
-  repo = "analysis";
-  owner = "math-comp";
-
-  release."1.14.0".hash = "sha256-FFcfxnF1wtz2e9Rdqu4Wd0rtLW0DYoXswCTji//RSCQ=";
-  release."1.13.0".hash = "sha256-nn2gl6cAO93QEdMvLGlB9WAPddQiOdeRtk1pLO+gxII=";
-  release."1.12.0".hash = "sha256-PF10NlZ+aqP3PX7+UsZwgJT9PEaDwzvrS/ZGzjP64Wo=";
-  release."1.11.0".hash = "sha256-1apbzBvaLNw/8ARLUhGGy89CyXW+/6O4ckdxKPraiVc=";
-  release."1.9.0".hash = "sha256-zj7WSDUg8ISWxcipGpjEwvvnLp1g8nm23BZiib/15+g=";
-  release."1.8.0".hash = "sha256-2ZafDmZAwGB7sxdUwNIE3xvwBRw1kFDk0m5Vz+onWZc=";
-  release."1.7.0".hash = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ=";
-  release."1.5.0".hash = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88=";
-  release."1.4.0".hash = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg=";
-  release."1.2.0".hash = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo=";
-  release."1.1.0".hash = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o=";
-  release."1.0.0".hash = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4=";
-  release."0.7.0".hash = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60=";
-  release."0.6.7".hash = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA=";
-  release."0.6.6".hash = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
-  release."0.6.5".hash = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
-  release."0.6.1".hash = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
-  release."0.6.0".hash = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
-  release."0.5.3".hash = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
-  release."0.5.2".hash = "sha256:0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw";
-  release."0.5.1".hash = "sha256:1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68";
-  release."0.3.13".hash = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
-  release."0.3.10".hash = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
-  release."0.3.9".hash = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
-  release."0.3.6".hash = "sha256:0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
-  release."0.3.4".hash = "sha256:18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
-  release."0.3.3".hash = "sha256:1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
-  release."0.3.1".hash = "sha256:1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
-  release."0.2.3".hash = "sha256:0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
-
-  defaultVersion =
-    let
-      case = coq: mc: out: {
-        cases = [
-          coq
-          mc
-        ];
-        inherit out;
-      };
-    in
-    with lib.versions;
-    lib.switch
-      [ coq.coq-version mathcomp.version ]
-      [
-        (case (range "8.20" "9.1") (range "2.4.0" "2.5.0") "1.14.0")
-        (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.13.0")
-        (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0")
-        (case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0")
-        (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0")
-        (case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0")
-        (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7")
-        (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6")
-        (case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5")
-        (case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1")
-        (case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2")
-        (case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1")
-        (case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13")
-        (case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10")
-        (case (range "8.10" "8.12") "1.11.0" "0.3.3")
-        (case (range "8.10" "8.11") "1.11.0" "0.3.1")
-        (case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3")
-      ]
-      null;
-
-  # list of analysis packages sorted by dependency order
-  packages = {
-    "classical" = [ ];
-    "reals" = [ "classical" ];
-    "experimental-reals" = [ "reals" ];
-    "analysis" = [ "reals" ];
-    "reals-stdlib" = [ "reals" ];
-    "analysis-stdlib" = [
-      "analysis"
-      "reals-stdlib"
-    ];
-  };
-
-  mathcomp_ =
-    package:
-    let
-      classical-deps = [
-        mathcomp.ssreflect
-        mathcomp.algebra
-        mathcomp-finmap
-      ];
-      experimental-reals-deps = [ mathcomp-bigenough ];
-      analysis-deps = [
-        mathcomp.field
-        mathcomp-bigenough
-      ];
-      intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
-      pkgpath = lib.switch package [
-        {
-          case = "single";
-          out = ".";
-        }
-        {
-          case = "analysis";
-          out = "theories";
-        }
-        {
-          case = "experimental-reals";
-          out = "experimental_reals";
-        }
-        {
-          case = "reals-stdlib";
-          out = "reals_stdlib";
-        }
-        {
-          case = "analysis-stdlib";
-          out = "analysis_stdlib";
-        }
-      ] package;
-      pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
-      derivation = mkCoqDerivation {
-        inherit
-          version
-          pname
-          defaultVersion
-          release
-          repo
-          owner
-          ;
-
-        namePrefix = [
-          "coq"
-          "mathcomp"
-        ];
-
-        propagatedBuildInputs =
-          intra-deps
-          ++ lib.optionals (lib.elem package [
-            "classical"
-            "single"
-          ]) classical-deps
-          ++ lib.optionals (lib.elem package [
-            "experimental-reals"
-            "single"
-          ]) experimental-reals-deps
-          ++ lib.optionals (lib.elem package [
-            "analysis"
-            "single"
-          ]) analysis-deps
-          ++ lib.optional (lib.elem package [
-            "reals-stdlib"
-            "analysis-stdlib"
-            "single"
-          ]) stdlib;
-
-        preBuild = ''
-          cd ${pkgpath}
-        '';
-
-        meta = {
-          description = "Analysis library compatible with Mathematical Components";
-          maintainers = [ lib.maintainers.cohencyril ];
-          license = lib.licenses.cecill-c;
-        };
-
-        passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
-      };
-      # split packages didn't exist before 0.6, so building nothing in that case
-      patched-derivation1 = derivation.overrideAttrs (
-        o:
-        lib.optionalAttrs
-          (
-            o.pname != null
-            && o.pname != "mathcomp-analysis"
-            && o.version != null
-            && o.version != "dev"
-            && lib.versions.isLt "0.6" o.version
-          )
-          {
-            preBuild = "";
-            buildPhase = "echo doing nothing";
-            installPhase = "echo doing nothing";
-          }
-      );
-      patched-derivation2 = patched-derivation1.overrideAttrs (
-        o:
-        lib.optionalAttrs (
-          o.pname != null
-          && o.pname == "mathcomp-analysis"
-          && o.version != null
-          && o.version != "dev"
-          && lib.versions.isLt "0.6" o.version
-        ) { preBuild = ""; }
-      );
-      # only packages classical and analysis existed before 1.7, so building nothing in that case
-      patched-derivation3 = patched-derivation2.overrideAttrs (
-        o:
-        lib.optionalAttrs
-          (
-            o.pname != null
-            && o.pname != "mathcomp-classical"
-            && o.pname != "mathcomp-analysis"
-            && o.version != null
-            && o.version != "dev"
-            && lib.versions.isLt "1.7" o.version
-          )
-          {
-            preBuild = "";
-            buildPhase = "echo doing nothing";
-            installPhase = "echo doing nothing";
-          }
-      );
-      patched-derivation = patched-derivation3.overrideAttrs (
-        o:
-        lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
-          {
-            propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
-          }
-      );
-    in
-    patched-derivation;
-in
-# this is just a wrapper for rocqPackages.mathcomp-analysis for Rocq >= 9.0
-if
-  coq.rocqPackages ? mathcomp-analysis
-  && !(lib.elem version [
-    "1.12.0"
-    "1.13.0"
-    "1.14.0"
-    "1.15.0"
-  ])
-then
-  coq.rocqPackages.mathcomp-analysis.override {
-    inherit version single;
-    inherit
-      mathcomp
-      mathcomp-finmap
-      mathcomp-bigenough
-      stdlib
-      ;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  mathcomp_ (if single then "single" else "analysis")
diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
deleted file mode 100644
index 3ba007d9dd0a..000000000000
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ /dev/null
@@ -1,52 +0,0 @@
-{
-  coq,
-  mkCoqDerivation,
-  mathcomp-boot,
-  lib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-
-    namePrefix = [
-      "coq"
-      "mathcomp"
-    ];
-    pname = "bigenough";
-    owner = "math-comp";
-
-    release = {
-      "1.0.0".hash = "sha256:10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
-      "1.0.1".hash = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
-      "1.0.2".hash = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
-      "1.0.3".hash = "sha256-9ObUoaavnninL72r5iqkLz7lJBpcKXXi8LXKGhgx/N4=";
-    };
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (range "8.10" "9.1") "1.0.3")
-        (case (range "8.10" "9.1") "1.0.2")
-        (case (range "8.5" "8.14") "1.0.0")
-      ] null;
-
-    propagatedBuildInputs = [ mathcomp-boot ];
-
-    meta = {
-      description = "Small library to do epsilon - N reasonning";
-      license = lib.licenses.cecill-b;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.mathcomp-bigenough for Rocq >= 9.0
-if coq.rocqPackages ? mathcomp-bigenough then
-  coq.rocqPackages.mathcomp-bigenough.override {
-    inherit version mathcomp-boot;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
deleted file mode 100644
index 9d4353db428c..000000000000
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ /dev/null
@@ -1,79 +0,0 @@
-{
-  coq,
-  mkCoqDerivation,
-  mathcomp-boot,
-  lib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-
-    namePrefix = [
-      "coq"
-      "mathcomp"
-    ];
-    pname = "finmap";
-    owner = "math-comp";
-    inherit version;
-    defaultVersion =
-      let
-        case = coq: mc: out: {
-          cases = [
-            coq
-            mc
-          ];
-          inherit out;
-        };
-      in
-      with lib.versions;
-      lib.switch
-        [ coq.coq-version mathcomp-boot.version ]
-        [
-          (case (range "8.20" "9.1") (range "2.3" "2.5") "2.2.2")
-          (case (range "8.20" "9.1") (range "2.3" "2.4") "2.2.0")
-          (case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
-          (case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
-          (case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
-          (case (isGe "8.10") (range "1.11" "1.17") "1.5.1")
-          (case (range "8.7" "8.11") "1.11.0" "1.5.0")
-          (case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
-          (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
-          (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
-          (case (range "8.7" "8.9") "1.7.0" "1.1.0")
-          (case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
-        ]
-        null;
-    release = {
-      "2.2.2".hash = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
-      "2.2.0".hash = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
-      "2.1.0".hash = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
-      "2.0.0".hash = "sha256-0Wr1ZUYVuZH74vawO4EZlZ+K3kq+s1xEz/BfzyKj+wk=";
-      "1.5.2".hash = "sha256-0KmmSjc2AlUo6BKr9RZ4FjL9wlGISlTGU0X1Eu7l4sw=";
-      "1.5.1".hash = "sha256:0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
-      "1.5.0".hash = "sha256:0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
-      "1.4.1".hash = "sha256:0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
-      "1.4.0+coq-8.11".hash = "sha256:1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
-      "1.4.0".hash = "sha256:0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
-      "1.3.4".hash = "sha256:0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
-      "1.2.1".hash = "sha256:0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
-      "1.1.0".hash = "sha256:05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
-      "1.0.0".hash = "sha256:0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
-    };
-
-    propagatedBuildInputs = [ mathcomp-boot ];
-
-    meta = {
-      description = "Finset and finmap library";
-      license = lib.licenses.cecill-b;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.mathcomp-finmap for Rocq >= 9.0
-if coq.rocqPackages ? mathcomp-finmap then
-  coq.rocqPackages.mathcomp-finmap.override {
-    inherit version mathcomp-boot;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
deleted file mode 100644
index 1d079f651347..000000000000
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ /dev/null
@@ -1,95 +0,0 @@
-{
-  coq,
-  mkCoqDerivation,
-  mathcomp,
-  mathcomp-bigenough,
-  lib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-
-    namePrefix = [
-      "coq"
-      "mathcomp"
-    ];
-    pname = "real-closed";
-    owner = "math-comp";
-    inherit version;
-    release = {
-      "2.0.3".hash = "sha256-heZ7aZ7TO9YNAESIvbAc1qqzO91xMyLAox8VKueIk/s=";
-      "2.0.2".hash = "sha256-hBo9JMtmXDYBmf5ihKGksQLHv3c0+zDBnd8/aI2V/ao=";
-      "2.0.1".hash = "sha256-tQTI3PCl0q1vWpps28oATlzOI8TpVQh1jhTwVmhaZic=";
-      "2.0.0".hash = "sha256-sZvfiC5+5Lg4nRhfKKqyFzovCj2foAhqaq/w9F2bdU8=";
-      "1.1.4".hash = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4=";
-      "1.1.3".hash = "sha256:1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7";
-      "1.1.2".hash = "sha256:0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
-      "1.1.1".hash = "sha256:0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
-      "1.0.5".hash = "sha256:0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
-      "1.0.4".hash = "sha256:058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
-      "1.0.3".hash = "sha256:1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
-      "1.0.1".hash = "sha256:0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
-    };
-
-    defaultVersion =
-      let
-        case = coq: mc: out: {
-          cases = [
-            coq
-            mc
-          ];
-          inherit out;
-        };
-      in
-      with lib.versions;
-      lib.switch
-        [ coq.version mathcomp.version ]
-        [
-          (case (range "8.18" "9.1") (isGe "2.2.0") "2.0.3")
-          (case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.0.2")
-          (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "2.0.1")
-          (case (range "8.16" "8.19") (range "2.0.0" "2.2.0") "2.0.0")
-          (case (range "8.13" "8.19") (range "1.13.0" "1.19.0") "1.1.4")
-          (case (isGe "8.13") (range "1.12.0" "1.18.0") "1.1.3")
-          (case (isGe "8.10") (range "1.12.0" "1.18.0") "1.1.2")
-          (case (isGe "8.7") "1.11.0" "1.1.1")
-          (case (isGe "8.7") (range "1.9.0" "1.10.0") "1.0.4")
-          (case (isGe "8.7") "1.8.0" "1.0.3")
-          (case (isGe "8.7") "1.7.0" "1.0.1")
-        ]
-        null;
-
-    propagatedBuildInputs = [
-      mathcomp.ssreflect
-      mathcomp.algebra
-      mathcomp.field
-      mathcomp.fingroup
-      mathcomp.solvable
-      mathcomp-bigenough
-    ];
-
-    meta = {
-      description = "Mathematical Components Library on real closed fields";
-      license = lib.licenses.cecill-c;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.mathcomp-real-closed for Rocq >= 9.0
-if
-  coq.rocqPackages ? mathcomp-real-closed
-  && !(lib.elem version [
-    "2.0.2"
-    "2.0.3"
-  ])
-then
-  coq.rocqPackages.mathcomp-real-closed.override {
-    inherit version;
-    inherit
-      mathcomp
-      mathcomp-bigenough
-      ;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
deleted file mode 100644
index c7c7334dc152..000000000000
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ /dev/null
@@ -1,285 +0,0 @@
-############################################################################
-# This file mainly provides the `mathcomp` derivation, which is            #
-# essentially a meta-package containing all core mathcomp libraries        #
-# (ssreflect fingroup algebra solvable field character). They can be       #
-# accessed individually through the passthrough attributes of mathcomp     #
-# bearing the same names (mathcomp.ssreflect, etc).                        #
-############################################################################
-# Compiling a custom version of mathcomp using `mathcomp.override`.        #
-# This is the replacement for the former `mathcomp_ config` function.      #
-# See the documentation at doc/languages-frameworks/coq.section.md.        #
-############################################################################
-
-{
-  lib,
-  ncurses,
-  graphviz,
-  lua,
-  fetchzip,
-  mkCoqDerivation,
-  withDoc ? false,
-  single ? false,
-  coq,
-  hierarchy-builder,
-  stdlib,
-  version ? null,
-}@args:
-
-let
-  repo = "math-comp";
-  owner = "math-comp";
-  withDoc = single && (args.withDoc or false);
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-      inherit (lib.versions) range;
-    in
-    lib.switch coq.coq-version [
-      (case (range "8.20" "9.1") "2.5.0")
-      (case (range "8.20" "9.1") "2.4.0")
-      (case (range "8.19" "9.0") "2.3.0")
-      (case (range "8.17" "8.20") "2.2.0")
-      (case (range "8.17" "8.18") "2.1.0")
-      (case (range "8.17" "8.18") "2.0.0")
-      (case (range "8.19" "8.20") "1.19.0")
-      (case (range "8.17" "8.18") "1.18.0")
-      (case (range "8.15" "8.18") "1.17.0")
-      (case (range "8.13" "8.18") "1.16.0")
-      (case (range "8.14" "8.16") "1.15.0")
-      (case (range "8.11" "8.15") "1.14.0")
-      (case (range "8.11" "8.15") "1.13.0")
-      (case (range "8.10" "8.13") "1.12.0")
-      (case (range "8.7" "8.12") "1.11.0")
-      (case (range "8.7" "8.11") "1.10.0")
-      (case (range "8.7" "8.11") "1.9.0")
-      (case (range "8.7" "8.9") "1.8.0")
-      (case (range "8.6" "8.9") "1.7.0")
-      (case (range "8.5" "8.7") "1.6.4")
-    ] null;
-  release = {
-    "2.5.0".hash = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";
-    "2.4.0".hash = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
-    "2.3.0".hash = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
-    "2.2.0".hash = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
-    "2.1.0".hash = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
-    "2.0.0".hash = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
-    "1.19.0".hash = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
-    "1.18.0".hash = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
-    "1.17.0".hash = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
-    "1.16.0".hash = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
-    "1.15.0".hash = "sha256:1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
-    "1.14.0".hash = "sha256:07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
-    "1.13.0".hash = "sha256:0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
-    "1.12.0".hash = "sha256:1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
-    "1.11.0".hash = "sha256:06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
-    "1.10.0".hash = "sha256:1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
-    "1.9.0".hash = "sha256:0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
-    "1.8.0".hash = "sha256:07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
-    "1.7.0".hash = "sha256:0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
-    "1.6.4".hash = "sha256:09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
-    "1.6.1".hash = "sha256:1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
-  };
-  releaseRev = v: "mathcomp-${v}";
-
-  # list of core mathcomp packages sorted by dependency order
-  packages = {
-    "boot" = [ ];
-    "order" = [ "boot" ];
-    "fingroup" = [ "boot" ];
-    "ssreflect" = [
-      "boot"
-      "order"
-    ];
-    "algebra" = [
-      "order"
-      "fingroup"
-    ];
-    "solvable" = [ "algebra" ];
-    "field" = [ "solvable" ];
-    "character" = [ "field" ];
-    "all" = [ "character" ];
-  };
-  meta = {
-    homepage = "https://math-comp.github.io/";
-    license = lib.licenses.cecill-b;
-    maintainers = with lib.maintainers; [
-      vbgl
-      jwiegley
-      cohencyril
-    ];
-  };
-
-  mathcomp_ =
-    package:
-    let
-      mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
-      pkgpath = if package == "single" then "." else package;
-      pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
-      pkgallMake = ''
-        echo "all.v"  > Make
-        echo "-I ." >>   Make
-        echo "-R . mathcomp.all" >> Make
-      '';
-      derivation = mkCoqDerivation (
-        {
-          inherit
-            version
-            pname
-            defaultVersion
-            release
-            releaseRev
-            repo
-            owner
-            meta
-            ;
-
-          mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
-          nativeBuildInputs = lib.optionals withDoc [
-            graphviz
-            lua
-          ];
-          buildInputs = [ ncurses ];
-          propagatedBuildInputs = mathcomp-deps;
-
-          buildFlags = lib.optional withDoc "doc";
-
-          preBuild = ''
-            if [[ -f etc/utils/ssrcoqdep ]]
-            then patchShebangs etc/utils/ssrcoqdep
-            fi
-            if [[ -f etc/buildlibgraph ]]
-            then patchShebangs etc/buildlibgraph
-            fi
-          ''
-          + ''
-            # handle mathcomp < 2.4.0 which had an extra base mathcomp directory
-            test -d mathcomp && cd mathcomp
-            cd ${pkgpath} || cd ssreflect  # before 2.5, boot didn't exist, make it behave as ssreflect
-          ''
-          + lib.optionalString (package == "all") pkgallMake;
-        }
-        // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
-        // lib.optionalAttrs withDoc {
-          htmldoc_template = fetchzip {
-            url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
-            hash = "sha256:0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
-          };
-          postBuild = ''
-            cp -rf _build_doc/* .
-            rm -r _build_doc
-          '';
-          postInstall =
-            let
-              tgt = "$out/share/coq/${coq.coq-version}/";
-            in
-            lib.optionalString withDoc ''
-              mkdir -p ${tgt}
-              cp -r htmldoc ${tgt}
-              cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
-            '';
-          buildTargets = "doc";
-          extraInstallFlags = [ "-f Makefile.coq" ];
-        }
-      );
-      patched-derivation1 = derivation.overrideAttrs (
-        o:
-        lib.optionalAttrs
-          (
-            o.pname != null
-            && o.pname == "mathcomp-all"
-            && o.version != null
-            && o.version != "dev"
-            && lib.versions.isLt "1.7" o.version
-          )
-          {
-            preBuild = "";
-            buildPhase = "";
-            installPhase = "echo doing nothing";
-          }
-      );
-      patched-derivation2 = patched-derivation1.overrideAttrs (
-        o:
-        lib.optionalAttrs
-          (
-            lib.versions.isLe "8.7" coq.coq-version || (o.version != "dev" && lib.versions.isLe "1.7" o.version)
-          )
-          {
-            installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
-          }
-      );
-      patched-derivation3 = patched-derivation2.overrideAttrs (
-        o:
-        lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
-          {
-            propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
-          }
-      );
-      patched-derivation4 = patched-derivation3.overrideAttrs (
-        o:
-        lib.optionalAttrs (o.version != null && o.version == "2.3.0") {
-          propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
-        }
-      );
-      # boot and order packages didn't exist before 2.5,
-      # so make boot behave as ssreflect then (c.f., above)
-      # and building nothing in order and ssreflect
-      patched-derivation5 = patched-derivation4.overrideAttrs (
-        o:
-        lib.optionalAttrs
-          (
-            lib.elem package [
-              "order"
-              "ssreflect"
-            ]
-            && o.version != null
-            && o.version != "dev"
-            && lib.versions.isLt "2.5" o.version
-          )
-          {
-            preBuild = "";
-            buildPhase = "echo doing nothing";
-            installPhase = "echo doing nothing";
-          }
-      );
-    in
-    patched-derivation5;
-in
-# this is just a wrapper for rocqPackages.mathcomp for Rocq >= 9.0
-if coq.rocqPackages ? mathcomp && version != "2.3.0" && version != "2.4.0" then
-  let
-    mc = coq.rocqPackages.mathcomp.override {
-      inherit version withDoc single;
-      inherit
-        ncurses
-        graphviz
-        lua
-        fetchzip
-        hierarchy-builder
-        ;
-      inherit (coq.rocqPackages) rocq-core micromega-plugin;
-    };
-  in
-  mc
-  // {
-    ssreflect = mkCoqDerivation {
-      inherit
-        version
-        defaultVersion
-        release
-        releaseRev
-        repo
-        owner
-        meta
-        ;
-      pname = "mathcomp-ssreflect";
-      propagatedBuildInputs = [
-        mc.boot
-        mc.order
-      ];
-      preBuild = "cd ssreflect";
-    };
-    fingroup = mc.finite-group;
-    character = mc.group-representation;
-  }
-else
-  mathcomp_ (if single then "single" else "all")
diff --git a/pkgs/development/coq-modules/parseque/default.nix b/pkgs/development/coq-modules/parseque/default.nix
deleted file mode 100644
index 98f8ab3f48e2..000000000000
--- a/pkgs/development/coq-modules/parseque/default.nix
+++ /dev/null
@@ -1,41 +0,0 @@
-{
-  lib,
-  mkCoqDerivation,
-  coq,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-    pname = "parseque";
-    repo = "parseque";
-    owner = "rocq-community";
-
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      lib.switch coq.coq-version [
-        (case (lib.versions.range "8.16" "8.20") "0.2.2")
-      ] null;
-
-    release."0.2.2".hash = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E=";
-
-    releaseRev = v: "v${v}";
-
-    meta = {
-      description = "Total parser combinators in Coq/Rocq";
-      maintainers = with lib.maintainers; [ womeier ];
-      license = lib.licenses.mit;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.parseque for Rocq >= 9.0
-if coq.rocqPackages ? parseque then
-  coq.rocqPackages.parseque.override {
-    inherit version;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix
deleted file mode 100644
index 3b3635d3ad36..000000000000
--- a/pkgs/development/coq-modules/relation-algebra/default.nix
+++ /dev/null
@@ -1,61 +0,0 @@
-{
-  lib,
-  mkCoqDerivation,
-  coq,
-  aac-tactics,
-  mathcomp-boot,
-  version ? null,
-}:
-
-mkCoqDerivation {
-  pname = "relation-algebra";
-  owner = "damien-pous";
-
-  releaseRev = v: if lib.versions.range "1.7.6" "1.7.9" v then "v.${v}" else "v${v}";
-
-  release."1.7.11".hash = "sha256-ZOV0lUdduSabW9Qsz70clkO7QK/NK2STaHqBWcXb7nI=";
-  release."1.7.10".hash = "sha256-h738L+dybhmWZwTSLJrhv+sB+cIbj0+62Zcy9BH5sVo=";
-  release."1.7.9".hash = "sha256-1WzAZyj6q7s0u/9r7lahzxTl8612EA540l9wpm7TYEg=";
-  release."1.7.8".hash = "sha256-RITFd3G5TjY+rFzW073Ao1AGU+u6OGQyQeGHVodAXnA=";
-  release."1.7.7".hash = "sha256:1dff3id6nypl2alhk9rcifj3dab0j78dym05blc525lawsmc26l2";
-  release."1.7.6".hash = "sha256:02gsj06zcy9zgd0h1ibqspwfiwm36pkkgg9cz37k4bxzcapxcr6w";
-  release."1.7.5".hash = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU=";
-  release."1.7.4".hash = "sha256-o+v2CIAa2+9tJ/V8DneDTf4k31KMHycgMBLaQ+A4ufM=";
-  release."1.7.3".hash = "sha256-4feSNfi7h4Yhwn5L+9KP9K1S7HCPvsvaVWwoQSTFvos=";
-  release."1.7.2".hash = "sha256-f4oNjXspNMEz3AvhIeYO3avbUa1AThoC9DbcHMb5A2o=";
-  release."1.7.1".hash = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA=";
-
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch coq.coq-version [
-      (case (isEq "8.20") "1.7.11")
-      (case (range "8.18" "8.19") "1.7.10")
-      (case (isEq "8.17") "1.7.9")
-      (case (isEq "8.16") "1.7.8")
-      (case (isEq "8.15") "1.7.7")
-      (case (isEq "8.14") "1.7.6")
-      (case (isEq "8.13") "1.7.5")
-      (case (isEq "8.12") "1.7.4")
-      (case (isEq "8.11") "1.7.3")
-      (case (isEq "8.10") "1.7.2")
-      (case (isEq "8.9") "1.7.1")
-    ] null;
-
-  mlPlugin = true;
-
-  propagatedBuildInputs = [
-    aac-tactics
-    mathcomp-boot
-  ];
-
-  meta = {
-    description = "Relation algebra library for Coq";
-    maintainers = with lib.maintainers; [ siraben ];
-    license = lib.licenses.gpl3Plus;
-    platforms = lib.platforms.unix;
-  };
-}
diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix
deleted file mode 100644
index 2871b536e839..000000000000
--- a/pkgs/development/coq-modules/stdlib/default.nix
+++ /dev/null
@@ -1,55 +0,0 @@
-{
-  coq,
-  mkCoqDerivation,
-  lib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-
-    pname = "stdlib";
-    repo = "stdlib";
-    owner = "coq";
-    opam-name = "coq-stdlib";
-
-    inherit version;
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (isLe "9.1") "9.0.0")
-        # the < 9.0 above is artificial as stdlib was included in Coq before
-      ] null;
-    releaseRev = v: "V${v}";
-
-    release."9.0.0".hash = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
-
-    configurePhase = ''
-      echo no configuration
-    '';
-    buildPhase = ''
-      echo building nothing
-    '';
-    installPhase = ''
-      echo installing nothing
-      # Make an output directory rather than a file, so this is more friendly to buildEnv
-      mkdir $out
-    '';
-
-    meta = {
-      description = "Compatibility metapackage for Coq Stdlib library after the Rocq renaming";
-      license = lib.licenses.lgpl21Only;
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0
-if coq.rocqPackages ? stdlib then
-  coq.rocqPackages.stdlib.override {
-    inherit version;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix
deleted file mode 100644
index 9f61637ce0ce..000000000000
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ /dev/null
@@ -1,65 +0,0 @@
-{
-  lib,
-  mkCoqDerivation,
-  coq,
-  stdlib,
-  version ? null,
-}:
-
-let
-  derivation = mkCoqDerivation {
-    pname = "stdpp";
-    inherit version;
-    domain = "gitlab.mpi-sws.org";
-    owner = "iris";
-    defaultVersion =
-      let
-        case = case: out: { inherit case out; };
-      in
-      with lib.versions;
-      lib.switch coq.coq-version [
-        (case (range "8.19" "9.1") "1.12.0")
-        (case (range "8.18" "8.19") "1.10.0")
-        (case (range "8.16" "8.18") "1.9.0")
-        (case (range "8.13" "8.17") "1.8.0")
-        (case (range "8.12" "8.14") "1.6.0")
-        (case (range "8.11" "8.13") "1.5.0")
-        (case (range "8.8" "8.10") "1.4.0")
-      ] null;
-    release."1.12.0".hash = "sha256-2o8YMkKbXrKHwtfpkdAovxl+2NZZk958GjSSd9wcEIU=";
-    release."1.11.0".hash = "sha256-yqnkaA5gUdZBJZ3JnvPYh11vKQRl0BAnior1yGowG7k=";
-    release."1.10.0".hash = "sha256-bfynevIKxAltvt76lsqVxBmifFkzEhyX8lRgTKxr21I=";
-    release."1.9.0".hash = "sha256-OXeB+XhdyzWMp5Karsz8obp0rTeMKrtG7fu/tmc9aeI=";
-    release."1.8.0".hash = "sha256-VkIGBPHevHeHCo/Q759Q7y9WyhSF/4SMht4cOPuAXHU=";
-    release."1.7.0".hash = "sha256:0447wbzm23f9rl8byqf6vglasfn6c1wy6cxrrwagqjwsh3i5lx8y";
-    release."1.6.0".hash = "sha256:1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v";
-    release."1.5.0".hash = "sha256:1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf";
-    release."1.4.0".hash = "sha256:1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
-    releaseRev = v: "coq-stdpp-${v}";
-
-    propagatedBuildInputs = [ stdlib ];
-
-    preBuild = ''
-      if [[ -f coq-lint.sh ]]
-      then patchShebangs coq-lint.sh
-      fi
-    '';
-
-    meta = {
-      description = "Extended “Standard Library” for Coq";
-      license = lib.licenses.bsd3;
-      maintainers = [
-        lib.maintainers.vbgl
-        lib.maintainers.ineol
-      ];
-    };
-  };
-in
-# this is just a wrapper for rocqPackages.stdpp for Rocq >= 9.0
-if coq.rocqPackages ? stdpp then
-  coq.rocqPackages.stdpp.override {
-    inherit version stdlib;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  derivation
diff --git a/pkgs/development/coq-modules/CakeMLExtraction/default.nix b/pkgs/development/rocq-modules/CakeMLExtraction/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/CakeMLExtraction/default.nix
rename to pkgs/development/rocq-modules/CakeMLExtraction/default.nix
diff --git a/pkgs/development/coq-modules/CertiRocq/default.nix b/pkgs/development/rocq-modules/CertiRocq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/CertiRocq/default.nix
rename to pkgs/development/rocq-modules/CertiRocq/default.nix
diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/rocq-modules/Cheerios/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/Cheerios/default.nix
rename to pkgs/development/rocq-modules/Cheerios/default.nix
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/rocq-modules/CoLoR/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/CoLoR/default.nix
rename to pkgs/development/rocq-modules/CoLoR/default.nix
diff --git a/pkgs/development/coq-modules/ConCert/default.nix b/pkgs/development/rocq-modules/ConCert/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ConCert/default.nix
rename to pkgs/development/rocq-modules/ConCert/default.nix
diff --git a/pkgs/development/coq-modules/ElmExtraction/default.nix b/pkgs/development/rocq-modules/ElmExtraction/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ElmExtraction/default.nix
rename to pkgs/development/rocq-modules/ElmExtraction/default.nix
diff --git a/pkgs/development/coq-modules/ExtLib/default.nix b/pkgs/development/rocq-modules/ExtLib/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ExtLib/default.nix
rename to pkgs/development/rocq-modules/ExtLib/default.nix
diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/rocq-modules/HoTT/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/HoTT/default.nix
rename to pkgs/development/rocq-modules/HoTT/default.nix
diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/rocq-modules/ITree/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ITree/default.nix
rename to pkgs/development/rocq-modules/ITree/default.nix
diff --git a/pkgs/development/coq-modules/InfSeqExt/default.nix b/pkgs/development/rocq-modules/InfSeqExt/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/InfSeqExt/default.nix
rename to pkgs/development/rocq-modules/InfSeqExt/default.nix
diff --git a/pkgs/development/coq-modules/LibHyps/default.nix b/pkgs/development/rocq-modules/LibHyps/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/LibHyps/default.nix
rename to pkgs/development/rocq-modules/LibHyps/default.nix
diff --git a/pkgs/development/coq-modules/MenhirLib/default.nix b/pkgs/development/rocq-modules/MenhirLib/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/MenhirLib/default.nix
rename to pkgs/development/rocq-modules/MenhirLib/default.nix
diff --git a/pkgs/development/coq-modules/Ordinal/default.nix b/pkgs/development/rocq-modules/Ordinal/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/Ordinal/default.nix
rename to pkgs/development/rocq-modules/Ordinal/default.nix
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/rocq-modules/QuickChick/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/QuickChick/default.nix
rename to pkgs/development/rocq-modules/QuickChick/default.nix
diff --git a/pkgs/development/coq-modules/RustExtraction/default.nix b/pkgs/development/rocq-modules/RustExtraction/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/RustExtraction/default.nix
rename to pkgs/development/rocq-modules/RustExtraction/default.nix
diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/rocq-modules/StructTact/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/StructTact/default.nix
rename to pkgs/development/rocq-modules/StructTact/default.nix
diff --git a/pkgs/development/coq-modules/TypedExtraction/default.nix b/pkgs/development/rocq-modules/TypedExtraction/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/TypedExtraction/default.nix
rename to pkgs/development/rocq-modules/TypedExtraction/default.nix
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/rocq-modules/VST/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/VST/default.nix
rename to pkgs/development/rocq-modules/VST/default.nix
diff --git a/pkgs/development/coq-modules/Velisarios/default.nix b/pkgs/development/rocq-modules/Velisarios/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/Velisarios/default.nix
rename to pkgs/development/rocq-modules/Velisarios/default.nix
diff --git a/pkgs/development/coq-modules/Verdi/default.nix b/pkgs/development/rocq-modules/Verdi/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/Verdi/default.nix
rename to pkgs/development/rocq-modules/Verdi/default.nix
diff --git a/pkgs/development/coq-modules/Vpl/default.nix b/pkgs/development/rocq-modules/Vpl/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/Vpl/default.nix
rename to pkgs/development/rocq-modules/Vpl/default.nix
diff --git a/pkgs/development/coq-modules/VplTactic/default.nix b/pkgs/development/rocq-modules/VplTactic/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/VplTactic/default.nix
rename to pkgs/development/rocq-modules/VplTactic/default.nix
diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/rocq-modules/aac-tactics/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/aac-tactics/default.nix
rename to pkgs/development/rocq-modules/aac-tactics/default.nix
diff --git a/pkgs/development/coq-modules/addition-chains/default.nix b/pkgs/development/rocq-modules/addition-chains/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/addition-chains/default.nix
rename to pkgs/development/rocq-modules/addition-chains/default.nix
diff --git a/pkgs/development/coq-modules/async-test/default.nix b/pkgs/development/rocq-modules/async-test/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/async-test/default.nix
rename to pkgs/development/rocq-modules/async-test/default.nix
diff --git a/pkgs/development/coq-modules/atbr/default.nix b/pkgs/development/rocq-modules/atbr/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/atbr/default.nix
rename to pkgs/development/rocq-modules/atbr/default.nix
diff --git a/pkgs/development/coq-modules/autosubst-ocaml/default.nix b/pkgs/development/rocq-modules/autosubst-ocaml/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/autosubst-ocaml/default.nix
rename to pkgs/development/rocq-modules/autosubst-ocaml/default.nix
diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/rocq-modules/autosubst/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/autosubst/default.nix
rename to pkgs/development/rocq-modules/autosubst/default.nix
diff --git a/pkgs/development/coq-modules/bbv/default.nix b/pkgs/development/rocq-modules/bbv/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/bbv/default.nix
rename to pkgs/development/rocq-modules/bbv/default.nix
diff --git a/pkgs/development/rocq-modules/bignums/default.nix b/pkgs/development/rocq-modules/bignums/default.nix
index f28cc74a3a55..a2b5d9783649 100644
--- a/pkgs/development/rocq-modules/bignums/default.nix
+++ b/pkgs/development/rocq-modules/bignums/default.nix
@@ -18,17 +18,42 @@ mkRocqDerivation {
     lib.switch rocq-core.rocq-version [
       (case (range "9.2" "9.3") "9.0.0+rocq9.2")
       (case (range "9.0" "9.1") "9.0.0+rocq${rocq-core.rocq-version}")
+      (case (range "8.13" "8.20") "9.0.0+coq${rocq-core.rocq-version}")
+      (case (range "8.6" "8.17") "${rocq-core.rocq-version}.0")
     ] null;
 
   release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
   release."9.0.0+rocq9.1".sha256 = "sha256-MSjlfJs3JOakuShOj+isNlus0bKlZ+rkvzRoKZQK5RQ=";
   release."9.0.0+rocq9.2".sha256 = "sha256-XQIx3MjmPgRsFMJiD1DR+FWkmO4J86tQ5fDuPHcjf+A=";
-  releaseRev = v: "v${v}";
+  release."9.0.0+coq8.20".hash = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";
+  release."9.0.0+coq8.19".hash = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ=";
+  release."9.0.0+coq8.18".hash = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8=";
+  release."9.0.0+coq8.17".hash = "sha256-Mn85LqxJKPDIfpxRef9Uh5POwOKlTQ7jsMVz1wnQwuY=";
+  release."9.0.0+coq8.16".hash = "sha256-pwFTl4Unr2ZIirAB3HTtfhL2YN7G/Pg88RX9AhKWXbE=";
+  release."9.0.0+coq8.15".hash = "sha256-2oGOANn3XULHNIlyqjZ5ppQTQa2QF1zzf3YjHAd/pjo=";
+  release."9.0.0+coq8.14".hash = "sha256-qTU152Dz34W6nFZ0pPbja9ouUm/714ZrLQ/Z4N/HIC4=";
+  release."9.0.0+coq8.13".hash = "sha256-zvAqV3VAB7cN+nlMhjSXzxuDkdd387ju2VSb2EUthI0=";
+  release."8.17.0".hash = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
+  release."8.16.0".hash = "sha256-DH3iWwatPlhhCVYVlgL2WLkvneSVzSXUiKo2e0+1zR4=";
+  release."8.15.0".hash = "sha256:093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";
+  release."8.14.0".hash = "sha256:0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06";
+  release."8.13.0".hash = "sha256:1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
+  release."8.12.0".hash = "sha256:14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
+  release."8.11.0".hash = "sha256:1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";
+  release."8.10.0".hash = "sha256:0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5";
+  release."8.9.0".hash = "sha256:03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01";
+  release."8.8.0".hash = "sha256:1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg";
+  release."8.7.0".hash = "sha256:11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl";
+  release."8.6.0".rev = "v8.6.0";
+  release."8.6.0".hash = "sha256:0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj";
+  releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}";
 
   mlPlugin = true;
 
   propagatedBuildInputs = [ stdlib ];
 
+  useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLt "9.0.0+rocq" v;
+
   meta = {
     license = lib.licenses.lgpl2;
   };
diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/rocq-modules/category-theory/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/category-theory/default.nix
rename to pkgs/development/rocq-modules/category-theory/default.nix
diff --git a/pkgs/development/coq-modules/ceres-bs/default.nix b/pkgs/development/rocq-modules/ceres-bs/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ceres-bs/default.nix
rename to pkgs/development/rocq-modules/ceres-bs/default.nix
diff --git a/pkgs/development/coq-modules/ceres/default.nix b/pkgs/development/rocq-modules/ceres/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ceres/default.nix
rename to pkgs/development/rocq-modules/ceres/default.nix
diff --git a/pkgs/development/coq-modules/coinduction/default.nix b/pkgs/development/rocq-modules/coinduction/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coinduction/default.nix
rename to pkgs/development/rocq-modules/coinduction/default.nix
diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/rocq-modules/compcert/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/compcert/default.nix
rename to pkgs/development/rocq-modules/compcert/default.nix
diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/rocq-modules/contribs/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/contribs/default.nix
rename to pkgs/development/rocq-modules/contribs/default.nix
diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/rocq-modules/coq-bits/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-bits/default.nix
rename to pkgs/development/rocq-modules/coq-bits/default.nix
diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/rocq-modules/coq-elpi/default.nix
similarity index 87%
rename from pkgs/development/coq-modules/coq-elpi/default.nix
rename to pkgs/development/rocq-modules/coq-elpi/default.nix
index bd751ed9d7fd..dd9ef20d8bd7 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/rocq-modules/coq-elpi/default.nix
@@ -139,29 +139,21 @@ let
       propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
     }
   );
-  patched-derivation4 = patched-derivation3.overrideAttrs (
-    o:
-    lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version))
-      {
-        configurePhase = ''
-          make dune-files || true
-        '';
-        buildPhase = ''
-          dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
-        '';
-        installPhase = ''
-          dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
-          mkdir $out/lib/coq/
-          mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
-        '';
-      }
-  );
 in
-# this is just a wrapper for rocqPackages.stdlib for Rocq >= 9.0
-if coq.rocqPackages ? rocq-elpi then
-  coq.rocqPackages.rocq-elpi.override {
-    inherit version elpi-version;
-    inherit (coq.rocqPackages) rocq-core;
-  }
-else
-  patched-derivation4
+patched-derivation3.overrideAttrs (
+  o:
+  lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.5.0" o.version))
+    {
+      configurePhase = ''
+        make dune-files || true
+      '';
+      buildPhase = ''
+        dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
+      '';
+      installPhase = ''
+        dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
+        mkdir $out/lib/coq/
+        mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
+      '';
+    }
+)
diff --git a/pkgs/development/coq-modules/coq-hammer/default.nix b/pkgs/development/rocq-modules/coq-hammer/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-hammer/default.nix
rename to pkgs/development/rocq-modules/coq-hammer/default.nix
diff --git a/pkgs/development/coq-modules/coq-hammer/tactics.nix b/pkgs/development/rocq-modules/coq-hammer/tactics.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-hammer/tactics.nix
rename to pkgs/development/rocq-modules/coq-hammer/tactics.nix
diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/rocq-modules/coq-haskell/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-haskell/default.nix
rename to pkgs/development/rocq-modules/coq-haskell/default.nix
diff --git a/pkgs/development/coq-modules/coq-lsp/coq-loader.patch b/pkgs/development/rocq-modules/coq-lsp/coq-loader.patch
similarity index 100%
rename from pkgs/development/coq-modules/coq-lsp/coq-loader.patch
rename to pkgs/development/rocq-modules/coq-lsp/coq-loader.patch
diff --git a/pkgs/development/coq-modules/coq-lsp/default.nix b/pkgs/development/rocq-modules/coq-lsp/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-lsp/default.nix
rename to pkgs/development/rocq-modules/coq-lsp/default.nix
diff --git a/pkgs/development/coq-modules/coq-matrix/default.nix b/pkgs/development/rocq-modules/coq-matrix/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-matrix/default.nix
rename to pkgs/development/rocq-modules/coq-matrix/default.nix
diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/rocq-modules/coq-record-update/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-record-update/default.nix
rename to pkgs/development/rocq-modules/coq-record-update/default.nix
diff --git a/pkgs/development/coq-modules/coq-tactical/default.nix b/pkgs/development/rocq-modules/coq-tactical/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coq-tactical/default.nix
rename to pkgs/development/rocq-modules/coq-tactical/default.nix
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/rocq-modules/coqeal/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coqeal/default.nix
rename to pkgs/development/rocq-modules/coqeal/default.nix
diff --git a/pkgs/development/coq-modules/coqfmt/default.nix b/pkgs/development/rocq-modules/coqfmt/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coqfmt/default.nix
rename to pkgs/development/rocq-modules/coqfmt/default.nix
diff --git a/pkgs/development/coq-modules/coqhammer/default.nix b/pkgs/development/rocq-modules/coqhammer/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coqhammer/default.nix
rename to pkgs/development/rocq-modules/coqhammer/default.nix
diff --git a/pkgs/development/coq-modules/coqide/default.nix b/pkgs/development/rocq-modules/coqide/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coqide/default.nix
rename to pkgs/development/rocq-modules/coqide/default.nix
diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/rocq-modules/coqprime/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coqprime/default.nix
rename to pkgs/development/rocq-modules/coqprime/default.nix
diff --git a/pkgs/development/coq-modules/coqtail-math/default.nix b/pkgs/development/rocq-modules/coqtail-math/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coqtail-math/default.nix
rename to pkgs/development/rocq-modules/coqtail-math/default.nix
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/rocq-modules/coquelicot/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coquelicot/default.nix
rename to pkgs/development/rocq-modules/coquelicot/default.nix
diff --git a/pkgs/development/coq-modules/coqutil/default.nix b/pkgs/development/rocq-modules/coqutil/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/coqutil/default.nix
rename to pkgs/development/rocq-modules/coqutil/default.nix
diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/rocq-modules/corn/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/corn/default.nix
rename to pkgs/development/rocq-modules/corn/default.nix
diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/rocq-modules/deriving/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/deriving/default.nix
rename to pkgs/development/rocq-modules/deriving/default.nix
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/rocq-modules/dpdgraph/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/dpdgraph/default.nix
rename to pkgs/development/rocq-modules/dpdgraph/default.nix
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/rocq-modules/equations/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/equations/default.nix
rename to pkgs/development/rocq-modules/equations/default.nix
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/rocq-modules/extructures/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/extructures/default.nix
rename to pkgs/development/rocq-modules/extructures/default.nix
diff --git a/pkgs/development/coq-modules/fcsl-pcm/default.nix b/pkgs/development/rocq-modules/fcsl-pcm/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/fcsl-pcm/default.nix
rename to pkgs/development/rocq-modules/fcsl-pcm/default.nix
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/rocq-modules/flocq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/flocq/default.nix
rename to pkgs/development/rocq-modules/flocq/default.nix
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/rocq-modules/fourcolor/default.nix
similarity index 98%
rename from pkgs/development/coq-modules/fourcolor/default.nix
rename to pkgs/development/rocq-modules/fourcolor/default.nix
index 8359575a4e32..198c7d4bac42 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/rocq-modules/fourcolor/default.nix
@@ -49,7 +49,7 @@ mkCoqDerivation {
 
   propagatedBuildInputs = [
     mathcomp.boot
-    mathcomp.fingroup
+    mathcomp.finite-group
     mathcomp.algebra
   ];
 
diff --git a/pkgs/development/coq-modules/gaia-hydras/default.nix b/pkgs/development/rocq-modules/gaia-hydras/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/gaia-hydras/default.nix
rename to pkgs/development/rocq-modules/gaia-hydras/default.nix
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/rocq-modules/gaia/default.nix
similarity index 98%
rename from pkgs/development/coq-modules/gaia/default.nix
rename to pkgs/development/rocq-modules/gaia/default.nix
index b048fe833367..c66bf8498920 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/rocq-modules/gaia/default.nix
@@ -46,7 +46,7 @@ mkCoqDerivation {
 
   propagatedBuildInputs = [
     mathcomp.boot
-    mathcomp.fingroup
+    mathcomp.finite-group
     mathcomp.algebra
     stdlib
   ];
diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/rocq-modules/gappalib/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/gappalib/default.nix
rename to pkgs/development/rocq-modules/gappalib/default.nix
diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/rocq-modules/goedel/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/goedel/default.nix
rename to pkgs/development/rocq-modules/goedel/default.nix
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/rocq-modules/graph-theory/default.nix
similarity index 98%
rename from pkgs/development/coq-modules/graph-theory/default.nix
rename to pkgs/development/rocq-modules/graph-theory/default.nix
index 6bf11119580d..0473fd29ff5e 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/rocq-modules/graph-theory/default.nix
@@ -51,7 +51,7 @@ mkCoqDerivation {
   propagatedBuildInputs = [
     mathcomp.algebra
     mathcomp-finmap
-    mathcomp.fingroup
+    mathcomp.finite-group
     fourcolor
     stdlib
   ]
diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/rocq-modules/heq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/heq/default.nix
rename to pkgs/development/rocq-modules/heq/default.nix
diff --git a/pkgs/development/rocq-modules/hierarchy-builder/default.nix b/pkgs/development/rocq-modules/hierarchy-builder/default.nix
index 9617bfc100e6..3ed67fea6b91 100644
--- a/pkgs/development/rocq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/rocq-modules/hierarchy-builder/default.nix
@@ -20,16 +20,38 @@ let
         (case (range "9.0" "9.3") "1.10.3")
         (case (range "9.0" "9.1") "1.10.2")
         (case (range "9.0" "9.1") "1.10.0")
-        (case (range "9.0" "9.1") "1.9.1")
+        (case (range "8.20" "9.1") "1.9.1")
+        (case (range "8.19" "8.20") "1.8.0")
+        (case (range "8.18" "8.20") "1.7.1")
+        (case (range "8.16" "8.18") "1.6.0")
+        (case (range "8.15" "8.18") "1.5.0")
+        (case (range "8.15" "8.17") "1.4.0")
+        (case (range "8.13" "8.14") "1.2.0")
+        (case (range "8.12" "8.13") "1.1.0")
+        (case (isEq "8.11") "0.10.0")
       ] null;
     release."1.10.3".hash = "sha256-y13KxzLulIu39Ci3aMc1cZG4tw3LL2ab7U9snI6jrXc=";
     release."1.10.2".sha256 = "sha256-Uzni9qrYQP45Tr+JkHs0BuRARwmWSMwA/iHhIzkolxc=";
     release."1.10.0".sha256 = "sha256-c52nS8I0tia7Q8lZTFJyHVPVabW9xv55m7w6B7y3+e8=";
     release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
+    release."1.8.0".hash = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
+    release."1.7.1".hash = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
+    release."1.7.0".hash = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
+    release."1.6.0".hash = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg=";
+    release."1.5.0".hash = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c=";
+    release."1.4.0".hash = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw=";
+    release."1.3.0".hash = "sha256:17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc";
+    release."1.2.1".hash = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0=";
+    release."1.2.0".hash = "sha256:0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d";
+    release."1.1.0".hash = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
+    release."1.0.0".hash = "sha256:0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";
+    release."0.10.0".hash = "sha256:1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
     releaseRev = v: "v${v}";
 
     propagatedBuildInputs = [ rocq-elpi ];
 
+    useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.9.1" v;
+
     meta = {
       description = "High level commands to declare a hierarchy based on packed classes";
       maintainers = with lib.maintainers; [
@@ -39,8 +61,19 @@ let
       license = lib.licenses.mit;
     };
   };
+  hb2 = hb.overrideAttrs (
+    o:
+    lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") {
+      buildPhase = "make build";
+    }
+    // (
+      if lib.versions.range "1.1.0" "1.9.1" o.version then
+        { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
+      else if lib.versions.range "0.10.0" "1.1.0" o.version then
+        { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }
+      else
+        { }
+    )
+  );
 in
-hb.overrideAttrs (
-  o:
-  lib.optionalAttrs (o.version == "1.9.1") { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
-)
+hb2
diff --git a/pkgs/development/coq-modules/high-school-geometry/default.nix b/pkgs/development/rocq-modules/high-school-geometry/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/high-school-geometry/default.nix
rename to pkgs/development/rocq-modules/high-school-geometry/default.nix
diff --git a/pkgs/development/coq-modules/http/default.nix b/pkgs/development/rocq-modules/http/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/http/default.nix
rename to pkgs/development/rocq-modules/http/default.nix
diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/rocq-modules/hydra-battles/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/hydra-battles/default.nix
rename to pkgs/development/rocq-modules/hydra-battles/default.nix
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/rocq-modules/interval/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/interval/default.nix
rename to pkgs/development/rocq-modules/interval/default.nix
diff --git a/pkgs/development/coq-modules/iris-named-props/default.nix b/pkgs/development/rocq-modules/iris-named-props/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/iris-named-props/default.nix
rename to pkgs/development/rocq-modules/iris-named-props/default.nix
diff --git a/pkgs/development/rocq-modules/iris/default.nix b/pkgs/development/rocq-modules/iris/default.nix
index b81ab29fa8bc..b72d89b48340 100644
--- a/pkgs/development/rocq-modules/iris/default.nix
+++ b/pkgs/development/rocq-modules/iris/default.nix
@@ -1,45 +1,62 @@
 {
   lib,
   mkRocqDerivation,
-  stdlib,
   rocq-core,
   stdpp,
   version ? null,
 }:
 
-mkRocqDerivation {
-  pname = "iris";
-  domain = "gitlab.mpi-sws.org";
-  owner = "iris";
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch rocq-core.rocq-version [
-      (case (range "9.0" "9.3") "4.5.0")
-    ] null;
-  release."4.5.0".sha256 = "sha256-oGqo+W1prLtAwRwo2U15VGhmrkDIPPE6uMbNrTa8iAQ=";
-  releaseRev = v: "iris-${v}";
+let
+  derivation = mkRocqDerivation {
+    pname = "iris";
+    domain = "gitlab.mpi-sws.org";
+    owner = "iris";
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      with lib.versions;
+      lib.switch rocq-core.rocq-version [
+        (case (range "9.0" "9.3") "4.5.0")
+        (case (range "8.19" "9.1") "4.4.0")
+        (case (range "8.18" "8.19") "4.2.0")
+        (case (range "8.16" "8.18") "4.1.0")
+        (case (range "8.13" "8.17") "4.0.0")
+        (case (range "8.12" "8.14") "3.5.0")
+        (case (range "8.11" "8.13") "3.4.0")
+        (case (range "8.9" "8.10") "3.3.0")
+      ] null;
+    release."4.5.0".sha256 = "sha256-oGqo+W1prLtAwRwo2U15VGhmrkDIPPE6uMbNrTa8iAQ=";
+    release."4.4.0".hash = "sha256-zpuaIdH2ScOuZB0Vt1TEHAbsmcT1DyoDsJpftT1M7qw=";
+    release."4.3.0".hash = "sha256-3qhjiFI+A3I3fD8rFfJL5Hek77wScfn/FNNbDyGqA1k=";
+    release."4.2.0".hash = "sha256-HuiHIe+5letgr1NN1biZZFq0qlWUbFmoVI7Q91+UIfM=";
+    release."4.1.0".hash = "sha256-nTZUeZOXiH7HsfGbMKDE7vGrNVCkbMaWxdMWUcTUNlo=";
+    release."4.0.0".hash = "sha256-Jc9TmgGvkiDaz9IOoExyeryU1E+Q37GN24NIM397/Gg=";
+    release."3.6.0".hash = "sha256:02vbq597fjxd5znzxdb54wfp36412wz2d4yash4q8yddgl1kakmj";
+    release."3.5.0".hash = "sha256:0hh14m0anfcv65rxm982ps2vp95vk9fwrpv4br8bxd9vz0091d70";
+    release."3.4.0".hash = "sha256:0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb";
+    release."3.3.0".hash = "sha256:0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";
+    releaseRev = v: "iris-${v}";
 
-  propagatedBuildInputs = [
-    stdlib
-    stdpp
-  ];
+    propagatedBuildInputs = [ stdpp ];
 
-  preBuild = ''
-    if [[ -f coq-lint.sh ]]
-    then patchShebangs coq-lint.sh
-    fi
-  '';
+    preBuild = ''
+      if [[ -f coq-lint.sh ]]
+      then patchShebangs coq-lint.sh
+      fi
+    '';
 
-  meta = {
-    description = "Rocq development of the Iris Project";
-    license = lib.licenses.bsd3;
-    maintainers = [
-      lib.maintainers.vbgl
-      lib.maintainers.ineol
-    ];
+    useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "4.4.0" v;
+
+    meta = {
+      description = "Rocq development of the Iris Project";
+      license = lib.licenses.bsd3;
+      maintainers = [
+        lib.maintainers.vbgl
+        lib.maintainers.ineol
+      ];
+    };
   };
-}
+in
+derivation
diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/rocq-modules/itauto/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/itauto/default.nix
rename to pkgs/development/rocq-modules/itauto/default.nix
diff --git a/pkgs/development/coq-modules/itauto/test.nix b/pkgs/development/rocq-modules/itauto/test.nix
similarity index 100%
rename from pkgs/development/coq-modules/itauto/test.nix
rename to pkgs/development/rocq-modules/itauto/test.nix
diff --git a/pkgs/development/coq-modules/itree-io/default.nix b/pkgs/development/rocq-modules/itree-io/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/itree-io/default.nix
rename to pkgs/development/rocq-modules/itree-io/default.nix
diff --git a/pkgs/development/coq-modules/jasmin/default.nix b/pkgs/development/rocq-modules/jasmin/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/jasmin/default.nix
rename to pkgs/development/rocq-modules/jasmin/default.nix
diff --git a/pkgs/development/coq-modules/json/default.nix b/pkgs/development/rocq-modules/json/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/json/default.nix
rename to pkgs/development/rocq-modules/json/default.nix
diff --git a/pkgs/development/coq-modules/lemma-overloading/default.nix b/pkgs/development/rocq-modules/lemma-overloading/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/lemma-overloading/default.nix
rename to pkgs/development/rocq-modules/lemma-overloading/default.nix
diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/rocq-modules/ltac2/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ltac2/default.nix
rename to pkgs/development/rocq-modules/ltac2/default.nix
diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/rocq-modules/math-classes/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/math-classes/default.nix
rename to pkgs/development/rocq-modules/math-classes/default.nix
diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/rocq-modules/mathcomp-abel/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/mathcomp-abel/default.nix
rename to pkgs/development/rocq-modules/mathcomp-abel/default.nix
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/rocq-modules/mathcomp-algebra-tactics/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
rename to pkgs/development/rocq-modules/mathcomp-algebra-tactics/default.nix
diff --git a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
index a1da2f0868b4..10b32be2a9b2 100644
--- a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
@@ -5,6 +5,7 @@
   mathcomp-finmap,
   mathcomp-bigenough,
   mathcomp-real-closed,
+  hierarchy-builder,
   stdlib,
   single ? false,
   rocq-core,
@@ -16,6 +17,35 @@ let
   owner = "math-comp";
 
   release."1.16.0".sha256 = "sha256-L0dCbxEqxI8rFv6OOEoIT/U3GKX37ageU9yw2H6hrWY=";
+  release."1.14.0".hash = "sha256-FFcfxnF1wtz2e9Rdqu4Wd0rtLW0DYoXswCTji//RSCQ=";
+  release."1.13.0".hash = "sha256-nn2gl6cAO93QEdMvLGlB9WAPddQiOdeRtk1pLO+gxII=";
+  release."1.12.0".hash = "sha256-PF10NlZ+aqP3PX7+UsZwgJT9PEaDwzvrS/ZGzjP64Wo=";
+  release."1.11.0".hash = "sha256-1apbzBvaLNw/8ARLUhGGy89CyXW+/6O4ckdxKPraiVc=";
+  release."1.9.0".hash = "sha256-zj7WSDUg8ISWxcipGpjEwvvnLp1g8nm23BZiib/15+g=";
+  release."1.8.0".hash = "sha256-2ZafDmZAwGB7sxdUwNIE3xvwBRw1kFDk0m5Vz+onWZc=";
+  release."1.7.0".hash = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ=";
+  release."1.5.0".hash = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88=";
+  release."1.4.0".hash = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg=";
+  release."1.2.0".hash = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo=";
+  release."1.1.0".hash = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o=";
+  release."1.0.0".hash = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4=";
+  release."0.7.0".hash = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60=";
+  release."0.6.7".hash = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA=";
+  release."0.6.6".hash = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
+  release."0.6.5".hash = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
+  release."0.6.1".hash = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
+  release."0.6.0".hash = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
+  release."0.5.3".hash = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
+  release."0.5.2".hash = "sha256:0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw";
+  release."0.5.1".hash = "sha256:1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68";
+  release."0.3.13".hash = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
+  release."0.3.10".hash = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
+  release."0.3.9".hash = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
+  release."0.3.6".hash = "sha256:0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
+  release."0.3.4".hash = "sha256:18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
+  release."0.3.3".hash = "sha256:1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
+  release."0.3.1".hash = "sha256:1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
+  release."0.2.3".hash = "sha256:0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
 
   defaultVersion =
     let
@@ -32,6 +62,23 @@ let
       [ rocq-core.rocq-version mathcomp.version ]
       [
         (case (range "9.0" "9.3") (range "2.4.0" "2.6.0") "1.16.0")
+        (case (range "8.20" "9.1") (range "2.4.0" "2.5.0") "1.14.0")
+        (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.13.0")
+        (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0")
+        (case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0")
+        (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0")
+        (case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0")
+        (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7")
+        (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6")
+        (case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5")
+        (case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1")
+        (case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2")
+        (case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1")
+        (case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13")
+        (case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10")
+        (case (range "8.10" "8.12") "1.11.0" "0.3.3")
+        (case (range "8.10" "8.11") "1.11.0" "0.3.1")
+        (case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3")
       ]
       null;
 
@@ -113,6 +160,8 @@ let
           cd ${pkgpath}
         '';
 
+        useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.15.0" v;
+
         meta = {
           description = "Analysis library compatible with Mathematical Components";
           maintainers = [ lib.maintainers.cohencyril ];
@@ -121,7 +170,59 @@ let
 
         passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
       };
+      # split packages didn't exist before 0.6, so building nothing in that case
+      patched-derivation1 = derivation.overrideAttrs (
+        o:
+        lib.optionalAttrs
+          (
+            o.pname != null
+            && o.pname != "mathcomp-analysis"
+            && o.version != null
+            && o.version != "dev"
+            && lib.versions.isLt "0.6" o.version
+          )
+          {
+            preBuild = "";
+            buildPhase = "echo doing nothing";
+            installPhase = "echo doing nothing";
+          }
+      );
+      patched-derivation2 = patched-derivation1.overrideAttrs (
+        o:
+        lib.optionalAttrs (
+          o.pname != null
+          && o.pname == "mathcomp-analysis"
+          && o.version != null
+          && o.version != "dev"
+          && lib.versions.isLt "0.6" o.version
+        ) { preBuild = ""; }
+      );
+      # only packages classical and analysis existed before 1.7, so building nothing in that case
+      patched-derivation3 = patched-derivation2.overrideAttrs (
+        o:
+        lib.optionalAttrs
+          (
+            o.pname != null
+            && o.pname != "mathcomp-classical"
+            && o.pname != "mathcomp-analysis"
+            && o.version != null
+            && o.version != "dev"
+            && lib.versions.isLt "1.7" o.version
+          )
+          {
+            preBuild = "";
+            buildPhase = "echo doing nothing";
+            installPhase = "echo doing nothing";
+          }
+      );
+      patched-derivation = patched-derivation3.overrideAttrs (
+        o:
+        lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
+          {
+            propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
+          }
+      );
     in
-    derivation;
+    patched-derivation;
 in
 mathcomp_ (if single then "single" else "analysis")
diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/rocq-modules/mathcomp-apery/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/mathcomp-apery/default.nix
rename to pkgs/development/rocq-modules/mathcomp-apery/default.nix
diff --git a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
index 0f6c1ce50129..924585a14513 100644
--- a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
@@ -6,32 +6,44 @@
   version ? null,
 }:
 
-mkRocqDerivation {
+let
+  derivation = mkRocqDerivation {
 
-  namePrefix = [
-    "rocq"
-    "mathcomp"
-  ];
-  pname = "bigenough";
-  owner = "math-comp";
+    namePrefix = [
+      "rocq"
+      "mathcomp"
+    ];
+    pname = "bigenough";
+    owner = "math-comp";
 
-  release = {
-    "1.0.4".sha256 = "sha256-cwfDCEFSXWnqV5aIrhTviUti0CXNwmFe6zVbqlD2iZw=";
+    release = {
+      "1.0.0".hash = "sha256:10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
+      "1.0.1".hash = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
+      "1.0.2".hash = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
+      "1.0.3".hash = "sha256-9ObUoaavnninL72r5iqkLz7lJBpcKXXi8LXKGhgx/N4=";
+      "1.0.4".sha256 = "sha256-cwfDCEFSXWnqV5aIrhTviUti0CXNwmFe6zVbqlD2iZw=";
+    };
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      with lib.versions;
+      lib.switch rocq-core.rocq-version [
+        (case (range "9.0" "9.3") "1.0.4")
+        (case (range "8.10" "9.1") "1.0.3")
+        (case (range "8.10" "9.1") "1.0.2")
+        (case (range "8.5" "8.14") "1.0.0")
+      ] null;
+
+    propagatedBuildInputs = [ mathcomp-boot ];
+
+    useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.0.3" v;
+
+    meta = {
+      description = "Small library to do epsilon - N reasonning";
+      license = lib.licenses.cecill-b;
+    };
   };
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch rocq-core.rocq-version [
-      (case (range "9.0" "9.3") "1.0.4")
-    ] null;
-
-  propagatedBuildInputs = [ mathcomp-boot ];
-
-  meta = {
-    description = "Small library to do epsilon - N reasonning";
-    license = lib.licenses.cecill-b;
-  };
-}
+in
+derivation
diff --git a/pkgs/development/rocq-modules/mathcomp-finmap/default.nix b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
index 440833462d4b..c520ddcd5354 100644
--- a/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
@@ -6,42 +6,71 @@
   version ? null,
 }:
 
-mkRocqDerivation {
+let
+  derivation = mkRocqDerivation {
 
-  namePrefix = [
-    "rocq"
-    "mathcomp"
-  ];
-  pname = "finmap";
-  owner = "math-comp";
-  inherit version;
-  defaultVersion =
-    let
-      case = rocq: mc: out: {
-        cases = [
-          rocq
-          mc
-        ];
-        inherit out;
-      };
-    in
-    with lib.versions;
-    lib.switch
-      [ rocq-core.rocq-version mathcomp-boot.version ]
-      [
-        (case (range "9.2" "9.3") (range "2.5" "2.6") "2.2.4") # also compiles on Rocq 9.0 and 9.1 (but requires graph-theory update)
-        (case (range "9.0" "9.1") (range "2.3" "2.5") "2.2.2")
-      ]
-      null;
-  release = {
-    "2.2.4".sha256 = "sha256-sEok7UhXiPdIH8/wzvVhXg1yprCETVmxMzeFRHh6Tug=";
-    "2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
+    namePrefix = [
+      "rocq"
+      "mathcomp"
+    ];
+    pname = "finmap";
+    owner = "math-comp";
+    inherit version;
+    defaultVersion =
+      let
+        case = rocq: mc: out: {
+          cases = [
+            rocq
+            mc
+          ];
+          inherit out;
+        };
+      in
+      with lib.versions;
+      lib.switch
+        [ rocq-core.rocq-version mathcomp-boot.version ]
+        [
+          (case (range "9.2" "9.3") (range "2.5" "2.6") "2.2.4") # also compiles on Rocq 9.0 and 9.1 (but requires graph-theory update)
+          (case (range "8.20" "9.1") (range "2.3" "2.5") "2.2.2")
+          (case (range "8.20" "9.1") (range "2.3" "2.4") "2.2.0")
+          (case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
+          (case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
+          (case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
+          (case (range "8.10" "8.15") (range "1.11" "1.17") "1.5.1")
+          (case (range "8.7" "8.11") "1.11.0" "1.5.0")
+          (case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
+          (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
+          (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
+          (case (range "8.7" "8.9") "1.7.0" "1.1.0")
+          (case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
+        ]
+        null;
+    release = {
+      "2.2.4".sha256 = "sha256-sEok7UhXiPdIH8/wzvVhXg1yprCETVmxMzeFRHh6Tug=";
+      "2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
+      "2.2.0".hash = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
+      "2.1.0".hash = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
+      "2.0.0".hash = "sha256-0Wr1ZUYVuZH74vawO4EZlZ+K3kq+s1xEz/BfzyKj+wk=";
+      "1.5.2".hash = "sha256-0KmmSjc2AlUo6BKr9RZ4FjL9wlGISlTGU0X1Eu7l4sw=";
+      "1.5.1".hash = "sha256:0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
+      "1.5.0".hash = "sha256:0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
+      "1.4.1".hash = "sha256:0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
+      "1.4.0+coq-8.11".hash = "sha256:1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
+      "1.4.0".hash = "sha256:0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
+      "1.3.4".hash = "sha256:0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
+      "1.2.1".hash = "sha256:0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
+      "1.1.0".hash = "sha256:05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
+      "1.0.0".hash = "sha256:0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
+    };
+
+    propagatedBuildInputs = [ mathcomp-boot ];
+
+    useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "2.2.2" v;
+
+    meta = {
+      description = "Finset and finmap library";
+      license = lib.licenses.cecill-b;
+    };
   };
-
-  propagatedBuildInputs = [ mathcomp-boot ];
-
-  meta = {
-    description = "Finset and finmap library";
-    license = lib.licenses.cecill-b;
-  };
-}
+in
+derivation
diff --git a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix b/pkgs/development/rocq-modules/mathcomp-infotheo/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/mathcomp-infotheo/default.nix
rename to pkgs/development/rocq-modules/mathcomp-infotheo/default.nix
diff --git a/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix
index bfa1f4bccbd2..fe81cb8877e2 100644
--- a/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix
@@ -7,46 +7,74 @@
   version ? null,
 }:
 
-mkRocqDerivation {
+let
+  derivation = mkRocqDerivation {
 
-  namePrefix = [
-    "rocq"
-    "mathcomp"
-  ];
-  pname = "real-closed";
-  owner = "math-comp";
-  inherit version;
-  release = {
-    "2.0.5".sha256 = "sha256-nns1TF3isv8FpWqtXilfMEVKvR50fvS6MXnYVzbCzVs=";
-    "2.0.6".sha256 = "sha256-c+0nlNTjTf115vjvnpLrgXye5YdjsWlsCBpGZj+hU9E=";
+    namePrefix = [
+      "rocq"
+      "mathcomp"
+    ];
+    pname = "real-closed";
+    owner = "math-comp";
+    inherit version;
+    release = {
+      "2.0.6".sha256 = "sha256-c+0nlNTjTf115vjvnpLrgXye5YdjsWlsCBpGZj+hU9E=";
+      "2.0.5".sha256 = "sha256-nns1TF3isv8FpWqtXilfMEVKvR50fvS6MXnYVzbCzVs=";
+      "2.0.3".hash = "sha256-heZ7aZ7TO9YNAESIvbAc1qqzO91xMyLAox8VKueIk/s=";
+      "2.0.2".hash = "sha256-hBo9JMtmXDYBmf5ihKGksQLHv3c0+zDBnd8/aI2V/ao=";
+      "2.0.1".hash = "sha256-tQTI3PCl0q1vWpps28oATlzOI8TpVQh1jhTwVmhaZic=";
+      "2.0.0".hash = "sha256-sZvfiC5+5Lg4nRhfKKqyFzovCj2foAhqaq/w9F2bdU8=";
+      "1.1.4".hash = "sha256-8Hs6XfowbpeRD8RhMRf4ZJe2xf8kE0e8m7bPUzR/IM4=";
+      "1.1.3".hash = "sha256:1vwmmnzy8i4f203i2s60dn9i0kr27lsmwlqlyyzdpsghvbr8h5b7";
+      "1.1.2".hash = "sha256:0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn";
+      "1.1.1".hash = "sha256:0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b";
+      "1.0.5".hash = "sha256:0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2";
+      "1.0.4".hash = "sha256:058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b";
+      "1.0.3".hash = "sha256:1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb";
+      "1.0.1".hash = "sha256:0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
+    };
+
+    defaultVersion =
+      let
+        case = rocq: mc: out: {
+          cases = [
+            rocq
+            mc
+          ];
+          inherit out;
+        };
+      in
+      with lib.versions;
+      lib.switch
+        [ rocq-core.version mathcomp.version ]
+        [
+          (case (range "9.0" "9.3") (isGe "2.6.0") "2.0.6")
+          (case (range "9.0" "9.2") (isEq "2.5.0") "2.0.5")
+          (case (range "8.18" "9.1") (isGe "2.2.0") "2.0.3")
+          (case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.0.2")
+          (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "2.0.1")
+          (case (range "8.16" "8.19") (range "2.0.0" "2.2.0") "2.0.0")
+          (case (range "8.13" "8.19") (range "1.13.0" "1.19.0") "1.1.4")
+          (case (isGe "8.13") (range "1.12.0" "1.18.0") "1.1.3")
+          (case (isGe "8.10") (range "1.12.0" "1.18.0") "1.1.2")
+          (case (isGe "8.7") "1.11.0" "1.1.1")
+          (case (isGe "8.7") (range "1.9.0" "1.10.0") "1.0.4")
+          (case (isGe "8.7") "1.8.0" "1.0.3")
+          (case (isGe "8.7") "1.7.0" "1.0.1")
+        ]
+        null;
+
+    propagatedBuildInputs = [
+      mathcomp.field
+      mathcomp-bigenough
+    ];
+
+    useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "2.0.3" v;
+
+    meta = {
+      description = "Mathematical Components Library on real closed fields";
+      license = lib.licenses.cecill-c;
+    };
   };
-
-  defaultVersion =
-    let
-      case = rocq: mc: out: {
-        cases = [
-          rocq
-          mc
-        ];
-        inherit out;
-      };
-    in
-    with lib.versions;
-    lib.switch
-      [ rocq-core.version mathcomp.version ]
-      [
-        (case (range "9.0" "9.3") (isGe "2.6.0") "2.0.6")
-        (case (range "9.0" "9.2") (isEq "2.5.0") "2.0.5")
-      ]
-      null;
-
-  propagatedBuildInputs = [
-    mathcomp.field
-    mathcomp-bigenough
-  ];
-
-  meta = {
-    description = "Mathematical Components Library on real closed fields";
-    license = lib.licenses.cecill-c;
-  };
-}
+in
+derivation
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/rocq-modules/mathcomp-tarjan/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/mathcomp-tarjan/default.nix
rename to pkgs/development/rocq-modules/mathcomp-tarjan/default.nix
diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/rocq-modules/mathcomp-word/default.nix
similarity index 98%
rename from pkgs/development/coq-modules/mathcomp-word/default.nix
rename to pkgs/development/rocq-modules/mathcomp-word/default.nix
index 0aa95dd0fead..42c411a43d87 100644
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-word/default.nix
@@ -81,7 +81,7 @@ mkCoqDerivation {
   propagatedBuildInputs = [
     mathcomp.algebra
     mathcomp.ssreflect
-    mathcomp.fingroup
+    mathcomp.finite-group
     stdlib
   ];
 
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/rocq-modules/mathcomp-zify/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/mathcomp-zify/default.nix
rename to pkgs/development/rocq-modules/mathcomp-zify/default.nix
diff --git a/pkgs/development/rocq-modules/mathcomp/default.nix b/pkgs/development/rocq-modules/mathcomp/default.nix
index 2b35e9ac3426..e08e3878d562 100644
--- a/pkgs/development/rocq-modules/mathcomp/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp/default.nix
@@ -21,7 +21,8 @@
   single ? false,
   rocq-core,
   hierarchy-builder,
-  micromega-plugin,
+  micromega-plugin ? null,
+  stdlib,
   version ? null,
 }@args:
 
@@ -36,11 +37,45 @@ let
     in
     lib.switch rocq-core.rocq-version [
       (case (range "9.2" "9.3") "2.6.0") # also compiles on Rocq 9.0 and 9.1
-      (case (range "9.0" "9.1") "2.5.0")
+      (case (range "8.20" "9.1") "2.5.0")
+      (case (range "8.20" "9.1") "2.4.0")
+      (case (range "8.19" "9.0") "2.3.0")
+      (case (range "8.17" "8.20") "2.2.0")
+      (case (range "8.17" "8.18") "2.1.0")
+      (case (range "8.17" "8.18") "2.0.0")
+      (case (range "8.19" "8.20") "1.19.0")
+      (case (range "8.17" "8.18") "1.18.0")
+      (case (range "8.15" "8.18") "1.17.0")
+      (case (range "8.13" "8.18") "1.16.0")
+      (case (range "8.14" "8.16") "1.15.0")
+      (case (range "8.11" "8.15") "1.14.0")
+      (case (range "8.11" "8.15") "1.13.0")
+      (case (range "8.10" "8.13") "1.12.0")
+      (case (range "8.7" "8.12") "1.11.0")
+      (case (range "8.7" "8.11") "1.10.0")
+      (case (range "8.7" "8.11") "1.9.0")
+      (case (range "8.7" "8.9") "1.8.0")
     ] null;
   release = {
     "2.6.0".sha256 = "sha256-SovoQ++213r8ISljts81j9E9G1vxVrFy+hhpsCw1fDY=";
     "2.5.0".sha256 = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";
+    "2.4.0".hash = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
+    "2.3.0".hash = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
+    "2.2.0".hash = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
+    "2.1.0".hash = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
+    "2.0.0".hash = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
+    "1.19.0".hash = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
+    "1.18.0".hash = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
+    "1.17.0".hash = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
+    "1.16.0".hash = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
+    "1.15.0".hash = "sha256:1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
+    "1.14.0".hash = "sha256:07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
+    "1.13.0".hash = "sha256:0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
+    "1.12.0".hash = "sha256:1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
+    "1.11.0".hash = "sha256:06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
+    "1.10.0".hash = "sha256:1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
+    "1.9.0".hash = "sha256:0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
+    "1.8.0".hash = "sha256:07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
   };
   releaseRev = v: "mathcomp-${v}";
 
@@ -48,6 +83,10 @@ let
   packages = {
     "boot" = [ ];
     "order" = [ "boot" ];
+    "ssreflect" = [
+      "boot"
+      "order"
+    ];
     "finite-group" = [ "boot" ];
     "algebra" = [
       "order"
@@ -66,6 +105,8 @@ let
       cdpkg =
         if package == "single" then
           "cd ."
+        else if package == "boot" then
+          "cd boot || cd ssreflect" # before 2.5, boot didn't exist, make it behave as ssreflect
         else if package == "group-representation" then
           "cd group_representation || cd character"
         else if package == "finite-group" then
@@ -95,20 +136,25 @@ let
             lua
           ];
           buildInputs = [ ncurses ];
-          propagatedBuildInputs = mathcomp-deps ++ [ hierarchy-builder ];
+          propagatedBuildInputs = mathcomp-deps;
 
           buildFlags = lib.optional withDoc "doc";
 
           preBuild = ''
+            if [[ -f etc/utils/ssrcoqdep ]]
+            then patchShebangs etc/utils/ssrcoqdep
+            fi
             if [[ -f etc/buildlibgraph ]]
             then patchShebangs etc/buildlibgraph
             fi
-          ''
-          + ''
+            # handle mathcomp < 2.4.0 which had an extra base mathcomp directory
+            test -d mathcomp && cd mathcomp
             ${cdpkg}
           ''
           + lib.optionalString (package == "all") pkgallMake;
 
+          useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLt "2.4.0" v;
+
           meta = {
             homepage = "https://math-comp.github.io/";
             license = lib.licenses.cecill-b;
@@ -143,6 +189,40 @@ let
         }
       );
       patched-derivation1 = derivation.overrideAttrs (
+        o:
+        lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
+          {
+            propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
+          }
+      );
+      patched-derivation2 = patched-derivation1.overrideAttrs (
+        o:
+        lib.optionalAttrs (o.version != null && o.version == "2.3.0") {
+          propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
+        }
+      );
+      # boot and order packages didn't exist before 2.5,
+      # so make boot behave as ssreflect then (c.f., above)
+      # and building nothing in order and ssreflect
+      patched-derivation3 = patched-derivation2.overrideAttrs (
+        o:
+        lib.optionalAttrs
+          (
+            lib.elem package [
+              "order"
+              "ssreflect"
+            ]
+            && o.version != null
+            && o.version != "dev"
+            && lib.versions.isLt "2.5" o.version
+          )
+          {
+            preBuild = "";
+            buildPhase = "echo doing nothing";
+            installPhase = "echo doing nothing";
+          }
+      );
+      patched-derivation4 = patched-derivation3.overrideAttrs (
         o:
         lib.optionalAttrs
           (
@@ -154,10 +234,11 @@ let
             && (o.version == "dev" || lib.versions.isGe "2.6.0" o.version)
           )
           {
-            propagatedBuildInputs = o.propagatedBuildInputs ++ [ micromega-plugin ];
+            propagatedBuildInputs =
+              o.propagatedBuildInputs ++ lib.optional (micromega-plugin != null) micromega-plugin;
           }
       );
     in
-    patched-derivation1;
+    patched-derivation4;
 in
 mathcomp_ (if single then "single" else "all")
diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/rocq-modules/metacoq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/metacoq/default.nix
rename to pkgs/development/rocq-modules/metacoq/default.nix
diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/rocq-modules/metalib/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/metalib/default.nix
rename to pkgs/development/rocq-modules/metalib/default.nix
diff --git a/pkgs/development/coq-modules/metarocq/default.nix b/pkgs/development/rocq-modules/metarocq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/metarocq/default.nix
rename to pkgs/development/rocq-modules/metarocq/default.nix
diff --git a/pkgs/development/coq-modules/mtac2/default.nix b/pkgs/development/rocq-modules/mtac2/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/mtac2/default.nix
rename to pkgs/development/rocq-modules/mtac2/default.nix
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/rocq-modules/multinomials/default.nix
similarity index 99%
rename from pkgs/development/coq-modules/multinomials/default.nix
rename to pkgs/development/rocq-modules/multinomials/default.nix
index f5add5287c63..5cf9ba36bcb4 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/rocq-modules/multinomials/default.nix
@@ -82,7 +82,7 @@ mkCoqDerivation {
     mathcomp.boot
     mathcomp.algebra
     mathcomp-finmap
-    mathcomp.fingroup
+    mathcomp.finite-group
     mathcomp-bigenough
   ];
 
diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/rocq-modules/odd-order/default.nix
similarity index 92%
rename from pkgs/development/coq-modules/odd-order/default.nix
rename to pkgs/development/rocq-modules/odd-order/default.nix
index 675b01928c93..7c9f3044069f 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/rocq-modules/odd-order/default.nix
@@ -2,7 +2,7 @@
   lib,
   coq,
   mkCoqDerivation,
-  mathcomp-character,
+  mathcomp-group-representation,
   version ? null,
 }:
 
@@ -32,7 +32,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch
-      [ coq.coq-version mathcomp-character.version ]
+      [ coq.coq-version mathcomp-group-representation.version ]
       [
         (case (range "9.1" "9.3") (range "2.5" "2.6") "2.4.0")
         (case (range "9.0" "9.1") (range "2.5" "2.5") "2.3.0")
@@ -45,7 +45,7 @@ mkCoqDerivation {
       null;
 
   propagatedBuildInputs = [
-    mathcomp-character
+    mathcomp-group-representation
   ];
 
   meta = {
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/rocq-modules/paco/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/paco/default.nix
rename to pkgs/development/rocq-modules/paco/default.nix
diff --git a/pkgs/development/coq-modules/paramcoq/default.nix b/pkgs/development/rocq-modules/paramcoq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/paramcoq/default.nix
rename to pkgs/development/rocq-modules/paramcoq/default.nix
diff --git a/pkgs/development/coq-modules/parsec/default.nix b/pkgs/development/rocq-modules/parsec/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/parsec/default.nix
rename to pkgs/development/rocq-modules/parsec/default.nix
diff --git a/pkgs/development/rocq-modules/parseque/default.nix b/pkgs/development/rocq-modules/parseque/default.nix
index 874fc0cbe496..818e7d042adc 100644
--- a/pkgs/development/rocq-modules/parseque/default.nix
+++ b/pkgs/development/rocq-modules/parseque/default.nix
@@ -6,31 +6,37 @@
   version ? null,
 }:
 
-mkRocqDerivation {
-  pname = "parseque";
-  repo = "parseque";
-  owner = "rocq-community";
+let
+  derivation = mkRocqDerivation {
+    pname = "parseque";
+    repo = "parseque";
+    owner = "rocq-community";
 
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch rocq-core.rocq-version [
-      (case (range "9.0" "9.3") "0.3.1")
-    ] null;
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      lib.switch rocq-core.rocq-version [
+        (case (lib.versions.range "9.0" "9.3") "0.3.1")
+        (case (lib.versions.range "8.16" "8.20") "0.2.2")
+      ] null;
 
-  release."0.3.0".sha256 = "sha256-W2eenv5Q421eVn2ubbninFmmdT875f3w/Zs7yGHUKP4=";
-  release."0.3.1".sha256 = "sha256-t7nHpHl6E3iXkhMO0A53URmKVpWENjf/VODVXjD9Y1A=";
+    release."0.2.2".hash = "sha256-O50Rs7Yf1H4wgwb7ltRxW+7IF0b04zpfs+mR83rxT+E=";
+    release."0.3.0".sha256 = "sha256-W2eenv5Q421eVn2ubbninFmmdT875f3w/Zs7yGHUKP4=";
+    release."0.3.1".sha256 = "sha256-t7nHpHl6E3iXkhMO0A53URmKVpWENjf/VODVXjD9Y1A=";
 
-  propagatedBuildInputs = [ stdlib ];
+    propagatedBuildInputs = [ stdlib ];
 
-  releaseRev = v: "v${v}";
+    releaseRev = v: "v${v}";
 
-  meta = {
-    description = "Total parser combinators in Rocq";
-    maintainers = with lib.maintainers; [ womeier ];
-    license = lib.licenses.mit;
+    useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "0.2.2" v;
+
+    meta = {
+      description = "Total parser combinators in Rocq";
+      maintainers = with lib.maintainers; [ womeier ];
+      license = lib.licenses.mit;
+    };
   };
-}
+in
+derivation
diff --git a/pkgs/development/coq-modules/pocklington/default.nix b/pkgs/development/rocq-modules/pocklington/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/pocklington/default.nix
rename to pkgs/development/rocq-modules/pocklington/default.nix
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/rocq-modules/reglang/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/reglang/default.nix
rename to pkgs/development/rocq-modules/reglang/default.nix
diff --git a/pkgs/development/rocq-modules/relation-algebra/default.nix b/pkgs/development/rocq-modules/relation-algebra/default.nix
index 73a712681bcf..189adb0b0116 100644
--- a/pkgs/development/rocq-modules/relation-algebra/default.nix
+++ b/pkgs/development/rocq-modules/relation-algebra/default.nix
@@ -3,6 +3,8 @@
   mkRocqDerivation,
   rocq-core,
   stdlib,
+  aac-tactics,
+  mathcomp-boot,
   version ? null,
 }:
 
@@ -12,21 +14,43 @@ mkRocqDerivation {
 
   inherit version;
   defaultVersion =
-    lib.switch
-      [ rocq-core.rocq-version ]
-      [
-        {
-          cases = [ (lib.versions.range "9.0" "9.1") ];
-          out = "1.8.0";
-        }
-      ]
-      null;
+    let
+      case = case: out: { inherit case out; };
+    in
+    with lib.versions;
+    lib.switch rocq-core.rocq-version [
+      (case (range "9.0" "9.1") "1.8.0")
+      (case (isEq "8.20") "1.7.11")
+      (case (range "8.18" "8.19") "1.7.10")
+      (case (isEq "8.17") "1.7.9")
+      (case (isEq "8.16") "1.7.8")
+      (case (isEq "8.15") "1.7.7")
+      (case (isEq "8.14") "1.7.6")
+      (case (isEq "8.13") "1.7.5")
+      (case (isEq "8.12") "1.7.4")
+      (case (isEq "8.11") "1.7.3")
+      (case (isEq "8.10") "1.7.2")
+      (case (isEq "8.9") "1.7.1")
+    ] null;
 
-  releaseRev = v: "v${v}";
+  releaseRev = v: if lib.versions.range "1.7.6" "1.7.9" v then "v.${v}" else "v${v}";
 
   release."1.8.0".sha256 = "sha256-RnY+a57KnStACteaT5dKQoCCH0qp7/W+4qoaApIilj0=";
+  release."1.7.11".hash = "sha256-ZOV0lUdduSabW9Qsz70clkO7QK/NK2STaHqBWcXb7nI=";
+  release."1.7.10".hash = "sha256-h738L+dybhmWZwTSLJrhv+sB+cIbj0+62Zcy9BH5sVo=";
+  release."1.7.9".hash = "sha256-1WzAZyj6q7s0u/9r7lahzxTl8612EA540l9wpm7TYEg=";
+  release."1.7.8".hash = "sha256-RITFd3G5TjY+rFzW073Ao1AGU+u6OGQyQeGHVodAXnA=";
+  release."1.7.7".hash = "sha256:1dff3id6nypl2alhk9rcifj3dab0j78dym05blc525lawsmc26l2";
+  release."1.7.6".hash = "sha256:02gsj06zcy9zgd0h1ibqspwfiwm36pkkgg9cz37k4bxzcapxcr6w";
+  release."1.7.5".hash = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU=";
+  release."1.7.4".hash = "sha256-o+v2CIAa2+9tJ/V8DneDTf4k31KMHycgMBLaQ+A4ufM=";
+  release."1.7.3".hash = "sha256-4feSNfi7h4Yhwn5L+9KP9K1S7HCPvsvaVWwoQSTFvos=";
+  release."1.7.2".hash = "sha256-f4oNjXspNMEz3AvhIeYO3avbUa1AThoC9DbcHMb5A2o=";
+  release."1.7.1".hash = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA=";
 
   propagatedBuildInputs = [
+    aac-tactics
+    mathcomp-boot
     stdlib
   ];
 
@@ -34,6 +58,8 @@ mkRocqDerivation {
 
   mlPlugin = true;
 
+  useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.7.11" v;
+
   meta = {
     description = "Relation algebra library for Rocq";
     maintainers = with lib.maintainers; [ siraben ];
diff --git a/pkgs/development/coq-modules/rewriter/default.nix b/pkgs/development/rocq-modules/rewriter/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/rewriter/default.nix
rename to pkgs/development/rocq-modules/rewriter/default.nix
diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/rocq-modules/semantics/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/semantics/default.nix
rename to pkgs/development/rocq-modules/semantics/default.nix
diff --git a/pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch b/pkgs/development/rocq-modules/serapi/8.10.0+0.7.2.patch
similarity index 100%
rename from pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch
rename to pkgs/development/rocq-modules/serapi/8.10.0+0.7.2.patch
diff --git a/pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch b/pkgs/development/rocq-modules/serapi/8.11.0+0.11.1.patch
similarity index 100%
rename from pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch
rename to pkgs/development/rocq-modules/serapi/8.11.0+0.11.1.patch
diff --git a/pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch b/pkgs/development/rocq-modules/serapi/8.12.0+0.12.1.patch
similarity index 100%
rename from pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch
rename to pkgs/development/rocq-modules/serapi/8.12.0+0.12.1.patch
diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/rocq-modules/serapi/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/serapi/default.nix
rename to pkgs/development/rocq-modules/serapi/default.nix
diff --git a/pkgs/development/coq-modules/serapi/janestreet-0.15.patch b/pkgs/development/rocq-modules/serapi/janestreet-0.15.patch
similarity index 100%
rename from pkgs/development/coq-modules/serapi/janestreet-0.15.patch
rename to pkgs/development/rocq-modules/serapi/janestreet-0.15.patch
diff --git a/pkgs/development/coq-modules/serapi/janestreet-0.16.patch b/pkgs/development/rocq-modules/serapi/janestreet-0.16.patch
similarity index 100%
rename from pkgs/development/coq-modules/serapi/janestreet-0.16.patch
rename to pkgs/development/rocq-modules/serapi/janestreet-0.16.patch
diff --git a/pkgs/development/coq-modules/serapi/sertop.patch b/pkgs/development/rocq-modules/serapi/sertop.patch
similarity index 100%
rename from pkgs/development/coq-modules/serapi/sertop.patch
rename to pkgs/development/rocq-modules/serapi/sertop.patch
diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/rocq-modules/simple-io/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/simple-io/default.nix
rename to pkgs/development/rocq-modules/simple-io/default.nix
diff --git a/pkgs/development/coq-modules/simple-io/test.nix b/pkgs/development/rocq-modules/simple-io/test.nix
similarity index 100%
rename from pkgs/development/coq-modules/simple-io/test.nix
rename to pkgs/development/rocq-modules/simple-io/test.nix
diff --git a/pkgs/development/coq-modules/smpl/default.nix b/pkgs/development/rocq-modules/smpl/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/smpl/default.nix
rename to pkgs/development/rocq-modules/smpl/default.nix
diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/rocq-modules/smtcoq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/smtcoq/default.nix
rename to pkgs/development/rocq-modules/smtcoq/default.nix
diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/rocq-modules/ssprove/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/ssprove/default.nix
rename to pkgs/development/rocq-modules/ssprove/default.nix
diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/rocq-modules/stalmarck/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/stalmarck/default.nix
rename to pkgs/development/rocq-modules/stalmarck/default.nix
diff --git a/pkgs/development/rocq-modules/stdlib/default.nix b/pkgs/development/rocq-modules/stdlib/default.nix
index b16f2903937f..7e97327c69a4 100644
--- a/pkgs/development/rocq-modules/stdlib/default.nix
+++ b/pkgs/development/rocq-modules/stdlib/default.nix
@@ -4,35 +4,58 @@
   lib,
   version ? null,
 }:
-mkRocqDerivation {
 
-  pname = "stdlib";
-  repo = "stdlib";
-  owner = "rocq-prover";
-  opam-name = "rocq-stdlib";
+let
+  derivation = mkRocqDerivation {
 
-  inherit version;
-  defaultVersion =
-    let
-      case = case: out: { inherit case out; };
-    in
-    with lib.versions;
-    lib.switch rocq-core.version [
-      (case (range "9.3" "9.3") "9.2.0")
-      (case (range "9.2" "9.2") "9.1.0")
-      (case (range "9.0" "9.1") "9.0.0")
-    ] null;
-  releaseRev = v: "V${v}";
+    pname = "stdlib";
+    repo = "stdlib";
+    owner = "rocq-prover";
+    opam-name = "rocq-stdlib";
 
-  release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
-  release."9.1.0".sha256 = "sha256-D/kCMsJDg5OnP37GhvXIr2Fi/xCbgCCzoikKx5rL6p4=";
-  release."9.2.0".sha256 = "sha256-ySNY8XUQOH6B1B2p+39jdJ7UjIMrRDl499JJwpLEHuM=";
+    inherit version;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      with lib.versions;
+      lib.switch rocq-core.version [
+        (case (range "9.3" "9.3") "9.2.0")
+        (case (range "9.2" "9.2") "9.1.0")
+        (case (isLe "9.1") "9.0.0")
+      ] null;
+    releaseRev = v: "V${v}";
 
-  mlPlugin = true;
+    release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
+    release."9.1.0".sha256 = "sha256-D/kCMsJDg5OnP37GhvXIr2Fi/xCbgCCzoikKx5rL6p4=";
+    release."9.2.0".sha256 = "sha256-ySNY8XUQOH6B1B2p+39jdJ7UjIMrRDl499JJwpLEHuM=";
+
+    mlPlugin = true;
+
+    meta = {
+      description = "Rocq Proof Assistant -- Standard Library";
+      license = lib.licenses.lgpl21Only;
+    };
 
-  meta = {
-    description = "Rocq Proof Assistant -- Standard Library";
-    license = lib.licenses.lgpl21Only;
   };
-
-}
+  # the < 9.0 above is artificial as stdlib was included in Coq before
+  patched-derivation = derivation.overrideAttrs (
+    o:
+    lib.optionalAttrs
+      (rocq-core.rocq-version != "dev" && lib.versions.isLe "8.20" rocq-core.rocq-version)
+      {
+        configurePhase = ''
+          echo no configuration
+        '';
+        buildPhase = ''
+          echo building nothing
+        '';
+        installPhase = ''
+          echo installing nothing
+          # Make an output directory rather than a file, so this is more friendly to buildEnv
+          mkdir $out
+        '';
+      }
+  );
+in
+patched-derivation
diff --git a/pkgs/development/rocq-modules/stdpp/default.nix b/pkgs/development/rocq-modules/stdpp/default.nix
index 89c1b1eae2c9..2c32d70f171d 100644
--- a/pkgs/development/rocq-modules/stdpp/default.nix
+++ b/pkgs/development/rocq-modules/stdpp/default.nix
@@ -18,8 +18,24 @@ mkRocqDerivation {
     with lib.versions;
     lib.switch rocq-core.rocq-version [
       (case (range "9.0" "9.3") "1.13.0")
+      (case (range "8.19" "9.1") "1.12.0")
+      (case (range "8.18" "8.19") "1.10.0")
+      (case (range "8.16" "8.18") "1.9.0")
+      (case (range "8.13" "8.17") "1.8.0")
+      (case (range "8.12" "8.14") "1.6.0")
+      (case (range "8.11" "8.13") "1.5.0")
+      (case (range "8.8" "8.10") "1.4.0")
     ] null;
   release."1.13.0".sha256 = "sha256-kj8oBzarsLB4DDQ43yz4ViQbyzuISqext28wC2Fh3Sw=";
+  release."1.12.0".hash = "sha256-2o8YMkKbXrKHwtfpkdAovxl+2NZZk958GjSSd9wcEIU=";
+  release."1.11.0".hash = "sha256-yqnkaA5gUdZBJZ3JnvPYh11vKQRl0BAnior1yGowG7k=";
+  release."1.10.0".hash = "sha256-bfynevIKxAltvt76lsqVxBmifFkzEhyX8lRgTKxr21I=";
+  release."1.9.0".hash = "sha256-OXeB+XhdyzWMp5Karsz8obp0rTeMKrtG7fu/tmc9aeI=";
+  release."1.8.0".hash = "sha256-VkIGBPHevHeHCo/Q759Q7y9WyhSF/4SMht4cOPuAXHU=";
+  release."1.7.0".hash = "sha256:0447wbzm23f9rl8byqf6vglasfn6c1wy6cxrrwagqjwsh3i5lx8y";
+  release."1.6.0".hash = "sha256:1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v";
+  release."1.5.0".hash = "sha256:1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf";
+  release."1.4.0".hash = "sha256:1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";
   releaseRev = v: "stdpp-${v}";
 
   propagatedBuildInputs = [ stdlib ];
@@ -30,6 +46,8 @@ mkRocqDerivation {
     fi
   '';
 
+  useCoqifVersion = v: v != null && v != "dev" && lib.versions.isLe "1.12.0" v;
+
   meta = {
     description = "Extended “Standard Library” for Rocq";
     license = lib.licenses.bsd3;
diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/rocq-modules/tlc/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/tlc/default.nix
rename to pkgs/development/rocq-modules/tlc/default.nix
diff --git a/pkgs/development/coq-modules/topology/default.nix b/pkgs/development/rocq-modules/topology/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/topology/default.nix
rename to pkgs/development/rocq-modules/topology/default.nix
diff --git a/pkgs/development/coq-modules/trakt/default.nix b/pkgs/development/rocq-modules/trakt/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/trakt/default.nix
rename to pkgs/development/rocq-modules/trakt/default.nix
diff --git a/pkgs/development/coq-modules/unicoq/default.nix b/pkgs/development/rocq-modules/unicoq/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/unicoq/default.nix
rename to pkgs/development/rocq-modules/unicoq/default.nix
diff --git a/pkgs/development/coq-modules/validsdp/default.nix b/pkgs/development/rocq-modules/validsdp/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/validsdp/default.nix
rename to pkgs/development/rocq-modules/validsdp/default.nix
diff --git a/pkgs/development/coq-modules/vcfloat/default.nix b/pkgs/development/rocq-modules/vcfloat/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/vcfloat/default.nix
rename to pkgs/development/rocq-modules/vcfloat/default.nix
diff --git a/pkgs/development/coq-modules/verified-extraction/default.nix b/pkgs/development/rocq-modules/verified-extraction/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/verified-extraction/default.nix
rename to pkgs/development/rocq-modules/verified-extraction/default.nix
diff --git a/pkgs/development/coq-modules/vscoq-language-server/default.nix b/pkgs/development/rocq-modules/vscoq-language-server/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/vscoq-language-server/default.nix
rename to pkgs/development/rocq-modules/vscoq-language-server/default.nix
diff --git a/pkgs/development/coq-modules/wasmcert/default.nix b/pkgs/development/rocq-modules/wasmcert/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/wasmcert/default.nix
rename to pkgs/development/rocq-modules/wasmcert/default.nix
diff --git a/pkgs/development/coq-modules/wasmcert/test.nix b/pkgs/development/rocq-modules/wasmcert/test.nix
similarity index 100%
rename from pkgs/development/coq-modules/wasmcert/test.nix
rename to pkgs/development/rocq-modules/wasmcert/test.nix
diff --git a/pkgs/development/coq-modules/waterproof/default.nix b/pkgs/development/rocq-modules/waterproof/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/waterproof/default.nix
rename to pkgs/development/rocq-modules/waterproof/default.nix
diff --git a/pkgs/development/coq-modules/zorns-lemma/default.nix b/pkgs/development/rocq-modules/zorns-lemma/default.nix
similarity index 100%
rename from pkgs/development/coq-modules/zorns-lemma/default.nix
rename to pkgs/development/rocq-modules/zorns-lemma/default.nix
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 53317c96c3dc..eb93cce8432d 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -10242,6 +10242,20 @@ with pkgs;
     rocq-core
     ;
 
+  inherit (rocqPackages) coq;
+
+  # Deprecated aliases
+
+  coqPackages = rocqPackages;
+  coqPackages_9_0 = rocqPackages_9_0;
+  coq_9_0 = rocqPackages_9_0.coq;
+  coqPackages_9_1 = rocqPackages_9_1;
+  coq_9_1 = rocqPackages_9_1.coq;
+  coqPackages_9_2 = rocqPackages_9_2;
+  coq_9_2 = rocqPackages_9_2.coq;
+  coqPackages_9_3 = rocqPackages_9_3;
+  coq_9_3 = rocqPackages_9_3.coq;
+
   inherit
     (callPackage ./coq-packages.nix {
       inherit (ocaml-ng)
@@ -10251,13 +10265,6 @@ with pkgs;
         ocamlPackages_4_14
         ocamlPackages_5_5
         ;
-      inherit
-        rocqPackages_9_0
-        rocqPackages_9_1
-        rocqPackages_9_2
-        rocqPackages_9_3
-        rocqPackages
-        ;
     })
     mkCoqPackages
     coqPackages_8_7
@@ -10288,16 +10295,6 @@ with pkgs;
     coq_8_19
     coqPackages_8_20
     coq_8_20
-    coqPackages_9_0
-    coq_9_0
-    coqPackages_9_1
-    coq_9_1
-    coqPackages_9_2
-    coq_9_2
-    coqPackages_9_3
-    coq_9_3
-    coqPackages
-    coq
     ;
 
   ekrhyper = callPackage ../applications/science/logic/ekrhyper {
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index ec4a42f8b692..1faa8097f120 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -65,33 +65,31 @@ let
         };
       });
 
-      contribs = lib.recurseIntoAttrs (callPackage ../development/coq-modules/contribs { });
+      rocq-core = coq;
 
-      aac-tactics = callPackage ../development/coq-modules/aac-tactics { };
-      addition-chains = callPackage ../development/coq-modules/addition-chains { };
-      async-test = callPackage ../development/coq-modules/async-test { };
-      atbr = callPackage ../development/coq-modules/atbr { };
-      autosubst = callPackage ../development/coq-modules/autosubst { };
-      autosubst-ocaml = callPackage ../development/coq-modules/autosubst-ocaml { };
-      bbv = callPackage ../development/coq-modules/bbv { };
-      bignums =
-        if lib.versionAtLeast coq.coq-version "8.6" then
-          callPackage ../development/coq-modules/bignums { }
-        else
-          null;
-      CakeMLExtraction = callPackage ../development/coq-modules/CakeMLExtraction { };
-      category-theory = callPackage ../development/coq-modules/category-theory { };
-      ceres = callPackage ../development/coq-modules/ceres { };
-      ceres-bs = callPackage ../development/coq-modules/ceres-bs { };
-      CertiRocq = callPackage ../development/coq-modules/CertiRocq { };
-      Cheerios = callPackage ../development/coq-modules/Cheerios { };
-      coinduction = callPackage ../development/coq-modules/coinduction { };
-      CoLoR = callPackage ../development/coq-modules/CoLoR (
+      contribs = lib.recurseIntoAttrs (callPackage ../development/rocq-modules/contribs { });
+
+      aac-tactics = callPackage ../development/rocq-modules/aac-tactics { };
+      addition-chains = callPackage ../development/rocq-modules/addition-chains { };
+      async-test = callPackage ../development/rocq-modules/async-test { };
+      atbr = callPackage ../development/rocq-modules/atbr { };
+      autosubst = callPackage ../development/rocq-modules/autosubst { };
+      autosubst-ocaml = callPackage ../development/rocq-modules/autosubst-ocaml { };
+      bbv = callPackage ../development/rocq-modules/bbv { };
+      bignums = callPackage ../development/rocq-modules/bignums { };
+      CakeMLExtraction = callPackage ../development/rocq-modules/CakeMLExtraction { };
+      category-theory = callPackage ../development/rocq-modules/category-theory { };
+      ceres = callPackage ../development/rocq-modules/ceres { };
+      ceres-bs = callPackage ../development/rocq-modules/ceres-bs { };
+      CertiRocq = callPackage ../development/rocq-modules/CertiRocq { };
+      Cheerios = callPackage ../development/rocq-modules/Cheerios { };
+      coinduction = callPackage ../development/rocq-modules/coinduction { };
+      CoLoR = callPackage ../development/rocq-modules/CoLoR (
         lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
           bignums = self.bignums.override { version = "8.13.0"; };
         }
       );
-      compcert = callPackage ../development/coq-modules/compcert {
+      compcert = callPackage ../development/rocq-modules/compcert {
         inherit
           fetchpatch
           makeWrapper
@@ -100,93 +98,94 @@ let
           stdenv
           ;
       };
-      ConCert = callPackage ../development/coq-modules/ConCert { };
-      coq-bits = callPackage ../development/coq-modules/coq-bits { };
-      coq-elpi = callPackage ../development/coq-modules/coq-elpi { };
-      coq-hammer = callPackage ../development/coq-modules/coq-hammer { };
-      coq-hammer-tactics = callPackage ../development/coq-modules/coq-hammer/tactics.nix { };
-      CoqMatrix = callPackage ../development/coq-modules/coq-matrix { };
-      coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
-      coq-lsp = callPackage ../development/coq-modules/coq-lsp { };
-      coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
-      coq-tactical = callPackage ../development/coq-modules/coq-tactical { };
-      coqeal = callPackage ../development/coq-modules/coqeal (
+      ConCert = callPackage ../development/rocq-modules/ConCert { };
+      coq-bits = callPackage ../development/rocq-modules/coq-bits { };
+      coq-elpi = callPackage ../development/rocq-modules/coq-elpi { };
+      rocq-elpi = callPackage ../development/rocq-modules/coq-elpi { };
+      coq-hammer = callPackage ../development/rocq-modules/coq-hammer { };
+      coq-hammer-tactics = callPackage ../development/rocq-modules/coq-hammer/tactics.nix { };
+      CoqMatrix = callPackage ../development/rocq-modules/coq-matrix { };
+      coq-haskell = callPackage ../development/rocq-modules/coq-haskell { };
+      coq-lsp = callPackage ../development/rocq-modules/coq-lsp { };
+      coq-record-update = callPackage ../development/rocq-modules/coq-record-update { };
+      coq-tactical = callPackage ../development/rocq-modules/coq-tactical { };
+      coqeal = callPackage ../development/rocq-modules/coqeal (
         lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) {
           bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; };
         }
       );
-      coqhammer = callPackage ../development/coq-modules/coqhammer { };
-      coqide = callPackage ../development/coq-modules/coqide { };
-      coqprime = callPackage ../development/coq-modules/coqprime { };
-      coqtail-math = callPackage ../development/coq-modules/coqtail-math { };
-      coquelicot = callPackage ../development/coq-modules/coquelicot { };
-      coqutil = callPackage ../development/coq-modules/coqutil { };
-      coqfmt = callPackage ../development/coq-modules/coqfmt { };
-      corn = callPackage ../development/coq-modules/corn { };
-      deriving = callPackage ../development/coq-modules/deriving { };
-      dpdgraph = callPackage ../development/coq-modules/dpdgraph { };
-      ElmExtraction = callPackage ../development/coq-modules/ElmExtraction { };
-      equations = callPackage ../development/coq-modules/equations { };
-      ExtLib = callPackage ../development/coq-modules/ExtLib { };
-      extructures = callPackage ../development/coq-modules/extructures { };
-      fcsl-pcm = callPackage ../development/coq-modules/fcsl-pcm { };
-      flocq = callPackage ../development/coq-modules/flocq { };
-      fourcolor = callPackage ../development/coq-modules/fourcolor { };
-      gaia = callPackage ../development/coq-modules/gaia { };
-      gaia-hydras = callPackage ../development/coq-modules/gaia-hydras { };
-      gappalib = callPackage ../development/coq-modules/gappalib { };
-      goedel = callPackage ../development/coq-modules/goedel { };
-      graph-theory = callPackage ../development/coq-modules/graph-theory { };
-      heq = callPackage ../development/coq-modules/heq { };
-      hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder { };
-      high-school-geometry = callPackage ../development/coq-modules/high-school-geometry { };
-      HoTT = callPackage ../development/coq-modules/HoTT { };
-      http = callPackage ../development/coq-modules/http { };
-      hydra-battles = callPackage ../development/coq-modules/hydra-battles { };
-      interval = callPackage ../development/coq-modules/interval { };
-      InfSeqExt = callPackage ../development/coq-modules/InfSeqExt { };
-      iris = callPackage ../development/coq-modules/iris { };
-      iris-named-props = callPackage ../development/coq-modules/iris-named-props { };
-      itauto = callPackage ../development/coq-modules/itauto { };
-      ITree = callPackage ../development/coq-modules/ITree { };
-      itree-io = callPackage ../development/coq-modules/itree-io { };
-      jasmin = callPackage ../development/coq-modules/jasmin { };
-      json = callPackage ../development/coq-modules/json { };
-      lemma-overloading = callPackage ../development/coq-modules/lemma-overloading { };
-      LibHyps = callPackage ../development/coq-modules/LibHyps { };
+      coqhammer = callPackage ../development/rocq-modules/coqhammer { };
+      coqide = callPackage ../development/rocq-modules/coqide { };
+      coqprime = callPackage ../development/rocq-modules/coqprime { };
+      coqtail-math = callPackage ../development/rocq-modules/coqtail-math { };
+      coquelicot = callPackage ../development/rocq-modules/coquelicot { };
+      coqutil = callPackage ../development/rocq-modules/coqutil { };
+      coqfmt = callPackage ../development/rocq-modules/coqfmt { };
+      corn = callPackage ../development/rocq-modules/corn { };
+      deriving = callPackage ../development/rocq-modules/deriving { };
+      dpdgraph = callPackage ../development/rocq-modules/dpdgraph { };
+      ElmExtraction = callPackage ../development/rocq-modules/ElmExtraction { };
+      equations = callPackage ../development/rocq-modules/equations { };
+      ExtLib = callPackage ../development/rocq-modules/ExtLib { };
+      extructures = callPackage ../development/rocq-modules/extructures { };
+      fcsl-pcm = callPackage ../development/rocq-modules/fcsl-pcm { };
+      flocq = callPackage ../development/rocq-modules/flocq { };
+      fourcolor = callPackage ../development/rocq-modules/fourcolor { };
+      gaia = callPackage ../development/rocq-modules/gaia { };
+      gaia-hydras = callPackage ../development/rocq-modules/gaia-hydras { };
+      gappalib = callPackage ../development/rocq-modules/gappalib { };
+      goedel = callPackage ../development/rocq-modules/goedel { };
+      graph-theory = callPackage ../development/rocq-modules/graph-theory { };
+      heq = callPackage ../development/rocq-modules/heq { };
+      hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };
+      high-school-geometry = callPackage ../development/rocq-modules/high-school-geometry { };
+      HoTT = callPackage ../development/rocq-modules/HoTT { };
+      http = callPackage ../development/rocq-modules/http { };
+      hydra-battles = callPackage ../development/rocq-modules/hydra-battles { };
+      interval = callPackage ../development/rocq-modules/interval { };
+      InfSeqExt = callPackage ../development/rocq-modules/InfSeqExt { };
+      iris = callPackage ../development/rocq-modules/iris { };
+      iris-named-props = callPackage ../development/rocq-modules/iris-named-props { };
+      itauto = callPackage ../development/rocq-modules/itauto { };
+      ITree = callPackage ../development/rocq-modules/ITree { };
+      itree-io = callPackage ../development/rocq-modules/itree-io { };
+      jasmin = callPackage ../development/rocq-modules/jasmin { };
+      json = callPackage ../development/rocq-modules/json { };
+      lemma-overloading = callPackage ../development/rocq-modules/lemma-overloading { };
+      LibHyps = callPackage ../development/rocq-modules/LibHyps { };
       libvalidsdp = self.validsdp.libvalidsdp;
-      ltac2 = callPackage ../development/coq-modules/ltac2 { };
-      math-classes = callPackage ../development/coq-modules/math-classes { };
-      mathcomp = callPackage ../development/coq-modules/mathcomp { };
+      ltac2 = callPackage ../development/rocq-modules/ltac2 { };
+      math-classes = callPackage ../development/rocq-modules/math-classes { };
+      mathcomp = callPackage ../development/rocq-modules/mathcomp { };
       ssreflect = self.mathcomp.ssreflect;
       mathcomp-boot = self.mathcomp.boot;
       mathcomp-order = self.mathcomp.order;
       mathcomp-ssreflect = self.mathcomp.ssreflect;
-      mathcomp-finite-group = self.mathcomp.fingroup;
-      mathcomp-fingroup = self.mathcomp.fingroup;
+      mathcomp-finite-group = self.mathcomp.finite-group;
+      mathcomp-fingroup = self.mathcomp.finite-group;
       mathcomp-algebra = self.mathcomp.algebra;
       mathcomp-solvable = self.mathcomp.solvable;
       mathcomp-field = self.mathcomp.field;
-      mathcomp-group-representation = self.mathcomp.character;
-      mathcomp-character = self.mathcomp.character;
-      mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel { };
-      mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics { };
-      mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis { };
+      mathcomp-group-representation = self.mathcomp.group-representation;
+      mathcomp-character = self.mathcomp.group-representation;
+      mathcomp-abel = callPackage ../development/rocq-modules/mathcomp-abel { };
+      mathcomp-algebra-tactics = callPackage ../development/rocq-modules/mathcomp-algebra-tactics { };
+      mathcomp-analysis = callPackage ../development/rocq-modules/mathcomp-analysis { };
       mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
-      mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery { };
-      mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough { };
+      mathcomp-apery = callPackage ../development/rocq-modules/mathcomp-apery { };
+      mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };
       mathcomp-classical = self.mathcomp-analysis.classical;
       mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
-      mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap { };
-      mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo { };
-      mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed { };
+      mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { };
+      mathcomp-infotheo = callPackage ../development/rocq-modules/mathcomp-infotheo { };
+      mathcomp-real-closed = callPackage ../development/rocq-modules/mathcomp-real-closed { };
       mathcomp-reals = self.mathcomp-analysis.reals;
       mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib;
-      mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan { };
-      mathcomp-word = callPackage ../development/coq-modules/mathcomp-word { };
-      mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify { };
-      MenhirLib = callPackage ../development/coq-modules/MenhirLib { };
-      metacoq = callPackage ../development/coq-modules/metacoq { };
+      mathcomp-tarjan = callPackage ../development/rocq-modules/mathcomp-tarjan { };
+      mathcomp-word = callPackage ../development/rocq-modules/mathcomp-word { };
+      mathcomp-zify = callPackage ../development/rocq-modules/mathcomp-zify { };
+      MenhirLib = callPackage ../development/rocq-modules/MenhirLib { };
+      metacoq = callPackage ../development/rocq-modules/metacoq { };
       metacoq-utils = self.metacoq.utils;
       metacoq-common = self.metacoq.common;
       metacoq-template-coq = self.metacoq.template-coq;
@@ -198,8 +197,8 @@ let
       metacoq-safechecker-plugin = self.metacoq.safechecker-plugin;
       metacoq-erasure-plugin = self.metacoq.erasure-plugin;
       metacoq-translations = self.metacoq.translations;
-      metalib = callPackage ../development/coq-modules/metalib { };
-      metarocq = callPackage ../development/coq-modules/metarocq { };
+      metalib = callPackage ../development/rocq-modules/metalib { };
+      metarocq = callPackage ../development/rocq-modules/metarocq { };
       metarocq-utils = self.metarocq.utils;
       metarocq-common = self.metarocq.common;
       metarocq-template-rocq = self.metarocq.template-rocq;
@@ -211,54 +210,54 @@ let
       metarocq-safechecker-plugin = self.metarocq.safechecker-plugin;
       metarocq-erasure-plugin = self.metarocq.erasure-plugin;
       metarocq-translations = self.metarocq.translations;
-      mtac2 = callPackage ../development/coq-modules/mtac2 { };
-      multinomials = callPackage ../development/coq-modules/multinomials { };
-      odd-order = callPackage ../development/coq-modules/odd-order { };
-      Ordinal = callPackage ../development/coq-modules/Ordinal { };
-      paco = callPackage ../development/coq-modules/paco { };
-      paramcoq = callPackage ../development/coq-modules/paramcoq { };
-      parsec = callPackage ../development/coq-modules/parsec { };
-      parseque = callPackage ../development/coq-modules/parseque { };
-      pocklington = callPackage ../development/coq-modules/pocklington { };
-      QuickChick = callPackage ../development/coq-modules/QuickChick { };
-      reglang = callPackage ../development/coq-modules/reglang { };
-      relation-algebra = callPackage ../development/coq-modules/relation-algebra { };
-      rewriter = callPackage ../development/coq-modules/rewriter { };
-      RustExtraction = callPackage ../development/coq-modules/RustExtraction { };
-      semantics = callPackage ../development/coq-modules/semantics { };
-      serapi = callPackage ../development/coq-modules/serapi { };
-      simple-io = callPackage ../development/coq-modules/simple-io { };
-      smpl = callPackage ../development/coq-modules/smpl { };
-      smtcoq = callPackage ../development/coq-modules/smtcoq { };
-      ssprove = callPackage ../development/coq-modules/ssprove { };
-      stalmarck-tactic = callPackage ../development/coq-modules/stalmarck { };
+      mtac2 = callPackage ../development/rocq-modules/mtac2 { };
+      multinomials = callPackage ../development/rocq-modules/multinomials { };
+      odd-order = callPackage ../development/rocq-modules/odd-order { };
+      Ordinal = callPackage ../development/rocq-modules/Ordinal { };
+      paco = callPackage ../development/rocq-modules/paco { };
+      paramcoq = callPackage ../development/rocq-modules/paramcoq { };
+      parsec = callPackage ../development/rocq-modules/parsec { };
+      parseque = callPackage ../development/rocq-modules/parseque { };
+      pocklington = callPackage ../development/rocq-modules/pocklington { };
+      QuickChick = callPackage ../development/rocq-modules/QuickChick { };
+      reglang = callPackage ../development/rocq-modules/reglang { };
+      relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
+      rewriter = callPackage ../development/rocq-modules/rewriter { };
+      RustExtraction = callPackage ../development/rocq-modules/RustExtraction { };
+      semantics = callPackage ../development/rocq-modules/semantics { };
+      serapi = callPackage ../development/rocq-modules/serapi { };
+      simple-io = callPackage ../development/rocq-modules/simple-io { };
+      smpl = callPackage ../development/rocq-modules/smpl { };
+      smtcoq = callPackage ../development/rocq-modules/smtcoq { };
+      ssprove = callPackage ../development/rocq-modules/ssprove { };
+      stalmarck-tactic = callPackage ../development/rocq-modules/stalmarck { };
       stalmarck = self.stalmarck-tactic.stalmarck;
-      stdlib = callPackage ../development/coq-modules/stdlib { };
-      stdpp = callPackage ../development/coq-modules/stdpp { };
-      StructTact = callPackage ../development/coq-modules/StructTact { };
-      tlc = callPackage ../development/coq-modules/tlc { };
-      topology = callPackage ../development/coq-modules/topology { };
-      trakt = callPackage ../development/coq-modules/trakt { };
-      TypedExtraction = callPackage ../development/coq-modules/TypedExtraction { };
+      stdlib = callPackage ../development/rocq-modules/stdlib { };
+      stdpp = callPackage ../development/rocq-modules/stdpp { };
+      StructTact = callPackage ../development/rocq-modules/StructTact { };
+      tlc = callPackage ../development/rocq-modules/tlc { };
+      topology = callPackage ../development/rocq-modules/topology { };
+      trakt = callPackage ../development/rocq-modules/trakt { };
+      TypedExtraction = callPackage ../development/rocq-modules/TypedExtraction { };
       TypedExtraction-common = self.TypedExtraction.common;
       TypedExtraction-elm = self.TypedExtraction.elm;
       TypedExtraction-rust = self.TypedExtraction.rust;
       TypedExtraction-plugin = self.TypedExtraction.plugin;
-      unicoq = callPackage ../development/coq-modules/unicoq { };
-      validsdp = callPackage ../development/coq-modules/validsdp { };
-      vcfloat = callPackage ../development/coq-modules/vcfloat (
+      unicoq = callPackage ../development/rocq-modules/unicoq { };
+      validsdp = callPackage ../development/rocq-modules/validsdp { };
+      vcfloat = callPackage ../development/rocq-modules/vcfloat (
         lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) {
           interval = self.interval.override { version = "4.9.0"; };
         }
       );
-      Velisarios = callPackage ../development/coq-modules/Velisarios { };
-      Verdi = callPackage ../development/coq-modules/Verdi { };
-      verified-extraction = callPackage ../development/coq-modules/verified-extraction { };
-      Vpl = callPackage ../development/coq-modules/Vpl { };
-      VplTactic = callPackage ../development/coq-modules/VplTactic { };
-      vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server { };
+      Velisarios = callPackage ../development/rocq-modules/Velisarios { };
+      Verdi = callPackage ../development/rocq-modules/Verdi { };
+      verified-extraction = callPackage ../development/rocq-modules/verified-extraction { };
+      Vpl = callPackage ../development/rocq-modules/Vpl { };
+      VplTactic = callPackage ../development/rocq-modules/VplTactic { };
+      vscoq-language-server = callPackage ../development/rocq-modules/vscoq-language-server { };
       vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { };
-      VST = callPackage ../development/coq-modules/VST (
+      VST = callPackage ../development/rocq-modules/VST (
         (lib.optionalAttrs (lib.versionAtLeast self.coq.version "8.14") {
           compcert = self.compcert.override {
             version =
@@ -282,9 +281,9 @@ let
           };
         })
       );
-      wasmcert = callPackage ../development/coq-modules/wasmcert { };
-      waterproof = callPackage ../development/coq-modules/waterproof { };
-      zorns-lemma = callPackage ../development/coq-modules/zorns-lemma { };
+      wasmcert = callPackage ../development/rocq-modules/wasmcert { };
+      waterproof = callPackage ../development/rocq-modules/waterproof { };
+      zorns-lemma = callPackage ../development/rocq-modules/zorns-lemma { };
       filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self;
     };
 
@@ -349,10 +348,6 @@ rec {
   coqPackages_8_18 = mkCoqPackages (mkCoq "8.18" { });
   coqPackages_8_19 = mkCoqPackages (mkCoq "8.19" { });
   coqPackages_8_20 = mkCoqPackages (mkCoq "8.20" { });
-  coqPackages_9_0 = mkCoqPackages (mkCoq "9.0" rocqPackages_9_0);
-  coqPackages_9_1 = mkCoqPackages (mkCoq "9.1" rocqPackages_9_1);
-  coqPackages_9_2 = mkCoqPackages (mkCoq "9.2" rocqPackages_9_2);
-  coqPackages_9_3 = mkCoqPackages (mkCoq "9.3" rocqPackages_9_3);
 
   coq_8_7 = coqPackages_8_7.coq;
   coq_8_8 = coqPackages_8_8.coq;
@@ -368,11 +363,5 @@ rec {
   coq_8_18 = coqPackages_8_18.coq;
   coq_8_19 = coqPackages_8_19.coq;
   coq_8_20 = coqPackages_8_20.coq;
-  coq_9_0 = coqPackages_9_0.coq;
-  coq_9_1 = coqPackages_9_1.coq;
-  coq_9_2 = coqPackages_9_2.coq;
-  coq_9_3 = coqPackages_9_3.coq;
 
-  coqPackages = lib.recurseIntoAttrs coqPackages_9_1;
-  coq = coqPackages.coq;
 }
diff --git a/pkgs/top-level/rocq-packages.nix b/pkgs/top-level/rocq-packages.nix
index d3adb57ae40e..8a8fd3fcaf55 100644
--- a/pkgs/top-level/rocq-packages.nix
+++ b/pkgs/top-level/rocq-packages.nix
@@ -9,6 +9,7 @@
   ocamlPackages_5_5,
   fetchpatch,
   makeWrapper,
+  coq2html,
 }@args:
 let
   lib = import ../build-support/rocq/extra-lib.nix { inherit (args) lib; };
@@ -20,7 +21,7 @@ let
       callPackage = self.callPackage;
     in
     {
-      inherit rocq-core lib;
+      inherit lib;
       rocqPackages = self // {
         __attrsFailEvaluation = true;
         recurseForDerivations = false;
@@ -36,36 +37,249 @@ let
       };
       mkRocqDerivation = lib.makeOverridable (callPackage ../build-support/rocq { });
 
+      coq = callPackage ../applications/science/logic/coq {
+        ocamlPackages_4_09 = null;
+        ocamlPackages_4_10 = null;
+        ocamlPackages_4_12 = null;
+        inherit ocamlPackages_4_14 ocamlPackages_5_5;
+        inherit (rocq-core) version;
+      };
+
+      mkCoqDerivation =
+        args:
+        self.mkRocqDerivation (
+          {
+            useCoq = true;
+            namePrefix = [ "coq" ];
+          }
+          // args
+        );
+
+      rocq-core = rocq-core.overrideAttrs (oldAttrs: {
+        passthru = (oldAttrs.passthru or { }) // {
+          withPackages =
+            f:
+            (callPackage ../applications/science/logic/coq/with-packages.nix {
+              coq = rocq-core;
+            })
+              (f self);
+        };
+      });
+
+      contribs = lib.recurseIntoAttrs (callPackage ../development/rocq-modules/contribs { });
+
+      aac-tactics = callPackage ../development/rocq-modules/aac-tactics { };
+      addition-chains = callPackage ../development/rocq-modules/addition-chains { };
+      async-test = callPackage ../development/rocq-modules/async-test { };
+      atbr = callPackage ../development/rocq-modules/atbr { };
+      autosubst = callPackage ../development/rocq-modules/autosubst { };
+      autosubst-ocaml = callPackage ../development/rocq-modules/autosubst-ocaml { };
+      bbv = callPackage ../development/rocq-modules/bbv { };
       bignums = callPackage ../development/rocq-modules/bignums { };
+      CakeMLExtraction = callPackage ../development/rocq-modules/CakeMLExtraction { };
+      category-theory = callPackage ../development/rocq-modules/category-theory { };
+      ceres = callPackage ../development/rocq-modules/ceres { };
+      ceres-bs = callPackage ../development/rocq-modules/ceres-bs { };
+      CertiRocq = callPackage ../development/rocq-modules/CertiRocq { };
+      Cheerios = callPackage ../development/rocq-modules/Cheerios { };
+      coinduction = callPackage ../development/rocq-modules/coinduction { };
+      CoLoR = callPackage ../development/rocq-modules/CoLoR { };
+      compcert = callPackage ../development/rocq-modules/compcert {
+        inherit
+          fetchpatch
+          makeWrapper
+          coq2html
+          lib
+          stdenv
+          ;
+      };
+      ConCert = callPackage ../development/rocq-modules/ConCert { };
+      coq-bits = callPackage ../development/rocq-modules/coq-bits { };
+      coq-hammer = callPackage ../development/rocq-modules/coq-hammer { };
+      coq-hammer-tactics = callPackage ../development/rocq-modules/coq-hammer/tactics.nix { };
+      CoqMatrix = callPackage ../development/rocq-modules/coq-matrix { };
+      coq-haskell = callPackage ../development/rocq-modules/coq-haskell { };
+      coq-lsp = callPackage ../development/rocq-modules/coq-lsp { };
+      coq-record-update = callPackage ../development/rocq-modules/coq-record-update { };
+      coq-tactical = callPackage ../development/rocq-modules/coq-tactical { };
+      coqeal = callPackage ../development/rocq-modules/coqeal (
+        lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) {
+          bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; };
+        }
+      );
+      coqhammer = callPackage ../development/rocq-modules/coqhammer { };
+      coqide = callPackage ../development/rocq-modules/coqide { };
+      coqprime = callPackage ../development/rocq-modules/coqprime { };
+      coqtail-math = callPackage ../development/rocq-modules/coqtail-math { };
+      coquelicot = callPackage ../development/rocq-modules/coquelicot { };
+      coqutil = callPackage ../development/rocq-modules/coqutil { };
+      coqfmt = callPackage ../development/rocq-modules/coqfmt { };
+      corn = callPackage ../development/rocq-modules/corn { };
+      deriving = callPackage ../development/rocq-modules/deriving { };
+      dpdgraph = callPackage ../development/rocq-modules/dpdgraph { };
+      ElmExtraction = callPackage ../development/rocq-modules/ElmExtraction { };
+      equations = callPackage ../development/rocq-modules/equations { };
+      ExtLib = callPackage ../development/rocq-modules/ExtLib { };
+      extructures = callPackage ../development/rocq-modules/extructures { };
+      fcsl-pcm = callPackage ../development/rocq-modules/fcsl-pcm { };
+      flocq = callPackage ../development/rocq-modules/flocq { };
+      fourcolor = callPackage ../development/rocq-modules/fourcolor { };
+      gaia = callPackage ../development/rocq-modules/gaia { };
+      gaia-hydras = callPackage ../development/rocq-modules/gaia-hydras { };
+      gappalib = callPackage ../development/rocq-modules/gappalib { };
+      goedel = callPackage ../development/rocq-modules/goedel { };
+      graph-theory = callPackage ../development/rocq-modules/graph-theory { };
+      heq = callPackage ../development/rocq-modules/heq { };
       hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { };
+      high-school-geometry = callPackage ../development/rocq-modules/high-school-geometry { };
+      HoTT = callPackage ../development/rocq-modules/HoTT { };
+      http = callPackage ../development/rocq-modules/http { };
+      hydra-battles = callPackage ../development/rocq-modules/hydra-battles { };
+      interval = callPackage ../development/rocq-modules/interval { };
+      InfSeqExt = callPackage ../development/rocq-modules/InfSeqExt { };
       iris = callPackage ../development/rocq-modules/iris { };
+      iris-named-props = callPackage ../development/rocq-modules/iris-named-props { };
+      itauto = callPackage ../development/rocq-modules/itauto { };
+      ITree = callPackage ../development/rocq-modules/ITree { };
+      itree-io = callPackage ../development/rocq-modules/itree-io { };
+      jasmin = callPackage ../development/rocq-modules/jasmin { };
+      json = callPackage ../development/rocq-modules/json { };
+      lemma-overloading = callPackage ../development/rocq-modules/lemma-overloading { };
+      LibHyps = callPackage ../development/rocq-modules/LibHyps { };
+      libvalidsdp = self.validsdp.libvalidsdp;
+      ltac2 = callPackage ../development/rocq-modules/ltac2 { };
+      math-classes = callPackage ../development/rocq-modules/math-classes { };
       mathcomp = callPackage ../development/rocq-modules/mathcomp { };
+      ssreflect = self.mathcomp.ssreflect;
       mathcomp-boot = self.mathcomp.boot;
       mathcomp-order = self.mathcomp.order;
+      mathcomp-ssreflect = self.mathcomp.ssreflect;
       mathcomp-finite-group = self.mathcomp.finite-group;
-      mathcomp-fingroup = self.mathcomp-finite-group;
+      mathcomp-fingroup = self.mathcomp.finite-group;
       mathcomp-algebra = self.mathcomp.algebra;
       mathcomp-solvable = self.mathcomp.solvable;
       mathcomp-field = self.mathcomp.field;
       mathcomp-group-representation = self.mathcomp.group-representation;
-      mathcomp-character = self.mathcomp-group-representation;
+      mathcomp-character = self.mathcomp.group-representation;
+      mathcomp-abel = callPackage ../development/rocq-modules/mathcomp-abel { };
+      mathcomp-algebra-tactics = callPackage ../development/rocq-modules/mathcomp-algebra-tactics { };
       mathcomp-analysis = callPackage ../development/rocq-modules/mathcomp-analysis { };
       mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;
+      mathcomp-apery = callPackage ../development/rocq-modules/mathcomp-apery { };
       mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };
       mathcomp-classical = self.mathcomp-analysis.classical;
       mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;
       mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { };
+      mathcomp-infotheo = callPackage ../development/rocq-modules/mathcomp-infotheo { };
       mathcomp-real-closed = callPackage ../development/rocq-modules/mathcomp-real-closed { };
       mathcomp-reals = self.mathcomp-analysis.reals;
       mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib;
+      mathcomp-tarjan = callPackage ../development/rocq-modules/mathcomp-tarjan { };
+      mathcomp-word = callPackage ../development/rocq-modules/mathcomp-word { };
+      mathcomp-zify = callPackage ../development/rocq-modules/mathcomp-zify { };
+      MenhirLib = callPackage ../development/rocq-modules/MenhirLib { };
+      metacoq = callPackage ../development/rocq-modules/metacoq { };
+      metacoq-utils = self.metacoq.utils;
+      metacoq-common = self.metacoq.common;
+      metacoq-template-coq = self.metacoq.template-coq;
+      metacoq-pcuic = self.metacoq.pcuic;
+      metacoq-safechecker = self.metacoq.safechecker;
+      metacoq-template-pcuic = self.metacoq.template-pcuic;
+      metacoq-erasure = self.metacoq.erasure;
+      metacoq-quotation = self.metacoq.quotation;
+      metacoq-safechecker-plugin = self.metacoq.safechecker-plugin;
+      metacoq-erasure-plugin = self.metacoq.erasure-plugin;
+      metacoq-translations = self.metacoq.translations;
+      metalib = callPackage ../development/rocq-modules/metalib { };
+      metarocq = callPackage ../development/rocq-modules/metarocq { };
+      metarocq-utils = self.metarocq.utils;
+      metarocq-common = self.metarocq.common;
+      metarocq-template-rocq = self.metarocq.template-rocq;
+      metarocq-pcuic = self.metarocq.pcuic;
+      metarocq-safechecker = self.metarocq.safechecker;
+      metarocq-template-pcuic = self.metarocq.template-pcuic;
+      metarocq-erasure = self.metarocq.erasure;
+      metarocq-quotation = self.metarocq.quotation;
+      metarocq-safechecker-plugin = self.metarocq.safechecker-plugin;
+      metarocq-erasure-plugin = self.metarocq.erasure-plugin;
+      metarocq-translations = self.metarocq.translations;
       micromega-plugin = callPackage ../development/rocq-modules/micromega-plugin { };
+      mtac2 = callPackage ../development/rocq-modules/mtac2 { };
+      multinomials = callPackage ../development/rocq-modules/multinomials { };
+      odd-order = callPackage ../development/rocq-modules/odd-order { };
+      Ordinal = callPackage ../development/rocq-modules/Ordinal { };
+      paco = callPackage ../development/rocq-modules/paco { };
+      paramcoq = callPackage ../development/rocq-modules/paramcoq { };
+      parsec = callPackage ../development/rocq-modules/parsec { };
       parseque = callPackage ../development/rocq-modules/parseque { };
+      pocklington = callPackage ../development/rocq-modules/pocklington { };
+      QuickChick = callPackage ../development/rocq-modules/QuickChick { };
+      reglang = callPackage ../development/rocq-modules/reglang { };
       relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
+      rewriter = callPackage ../development/rocq-modules/rewriter { };
       rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };
+      coq-elpi = self.rocq-elpi;
       rocqnavi = callPackage ../development/rocq-modules/rocqnavi { };
+      RustExtraction = callPackage ../development/rocq-modules/RustExtraction { };
+      semantics = callPackage ../development/rocq-modules/semantics { };
+      serapi = callPackage ../development/rocq-modules/serapi { };
+      simple-io = callPackage ../development/rocq-modules/simple-io { };
+      smpl = callPackage ../development/rocq-modules/smpl { };
+      smtcoq = callPackage ../development/rocq-modules/smtcoq { };
+      ssprove = callPackage ../development/rocq-modules/ssprove { };
+      stalmarck-tactic = callPackage ../development/rocq-modules/stalmarck { };
+      stalmarck = self.stalmarck-tactic.stalmarck;
       stdlib = callPackage ../development/rocq-modules/stdlib { };
       stdpp = callPackage ../development/rocq-modules/stdpp { };
+      StructTact = callPackage ../development/rocq-modules/StructTact { };
+      tlc = callPackage ../development/rocq-modules/tlc { };
+      topology = callPackage ../development/rocq-modules/topology { };
+      trakt = callPackage ../development/rocq-modules/trakt { };
+      TypedExtraction = callPackage ../development/rocq-modules/TypedExtraction { };
+      TypedExtraction-common = self.TypedExtraction.common;
+      TypedExtraction-elm = self.TypedExtraction.elm;
+      TypedExtraction-rust = self.TypedExtraction.rust;
+      TypedExtraction-plugin = self.TypedExtraction.plugin;
+      unicoq = callPackage ../development/rocq-modules/unicoq { };
+      validsdp = callPackage ../development/rocq-modules/validsdp { };
+      vcfloat = callPackage ../development/rocq-modules/vcfloat (
+        lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) {
+          interval = self.interval.override { version = "4.9.0"; };
+        }
+      );
+      Velisarios = callPackage ../development/rocq-modules/Velisarios { };
+      Verdi = callPackage ../development/rocq-modules/Verdi { };
+      verified-extraction = callPackage ../development/rocq-modules/verified-extraction { };
+      Vpl = callPackage ../development/rocq-modules/Vpl { };
+      VplTactic = callPackage ../development/rocq-modules/VplTactic { };
       vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { };
+      VST = callPackage ../development/rocq-modules/VST (
+        (lib.optionalAttrs (lib.versionAtLeast self.coq.version "8.14") {
+          compcert = self.compcert.override {
+            version =
+              with lib.versions;
+              lib.switch self.coq.version [
+                {
+                  case = range "8.15" "8.18";
+                  out = "3.13.1";
+                }
+                {
+                  case = isEq "8.14";
+                  out = "3.11";
+                }
+              ] null;
+          };
+        })
+        // (lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") {
+          ITree = self.ITree.override {
+            version = "4.0.0";
+            paco = self.paco.override { version = "4.1.2"; };
+          };
+        })
+      );
+      wasmcert = callPackage ../development/rocq-modules/wasmcert { };
+      waterproof = callPackage ../development/rocq-modules/waterproof { };
+      zorns-lemma = callPackage ../development/rocq-modules/zorns-lemma { };
 
       filterPackages = doesFilter: if doesFilter then filterRocqPackages self else self;
     };