diff --git a/doc/languages-frameworks/rocq.section.md b/doc/languages-frameworks/rocq.section.md
index 056394056797..b93a2b62e33e 100644
--- a/doc/languages-frameworks/rocq.section.md
+++ b/doc/languages-frameworks/rocq.section.md
@@ -59,7 +59,7 @@ The recommended way of defining a derivation for a Rocq library, is to use the `
 * `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags,
 * `releaseArtifact` (optional, defaults to `(v: null)`), provides a default mapping from release names to artifact names (only works for github artifact for now),
 * `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers,
-* `namePrefix` (optional, defaults to `[ "rocq-core" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
+* `namePrefix` (optional, defaults to `[ "rocq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
 * `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune`, `useDuneifVersion` and `mlPlugin` are set).
 * `extraNativeBuildInputs` (optional, deprecated), an additional list of derivation to add to `nativeBuildInputs`,
 * `overrideNativeBuildInputs` (optional) replaces the default list of derivation to which `nativeBuildInputs` and `extraNativeBuildInputs` adds extra elements,
diff --git a/pkgs/build-support/rocq/default.nix b/pkgs/build-support/rocq/default.nix
index 68181efcfb44..6a25a171cb25 100644
--- a/pkgs/build-support/rocq/default.nix
+++ b/pkgs/build-support/rocq/default.nix
@@ -55,7 +55,7 @@ in
   extraNativeBuildInputs ? [ ],
   overrideBuildInputs ? [ ],
   overrideNativeBuildInputs ? [ ],
-  namePrefix ? [ "rocq-core" ],
+  namePrefix ? null,
   enableParallelBuilding ? true,
   extraInstallFlags ? [ ],
   setROCQBIN ? true,
@@ -66,7 +66,7 @@ in
   dropDerivationAttrs ? [ ],
   useDuneifVersion ? (x: false),
   useDune ? false,
-  opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
+  opam-name ? null,
   useCoq ? false,
   useCoqifVersion ? (x: false),
   ...
@@ -160,10 +160,17 @@ let
       ] ""
     )
     + optionalString (v == null) "-broken";
-  append-version = p: n: p + display-pkg n "" rocqPackages.${n}.version + "-";
-  prefix-name = foldl append-version "" namePrefix;
   useDune = args.useDune or (useDuneifVersion fetched.version);
   useCoq = args.useCoq or (useCoqifVersion fetched.version);
+  namePrefix = args.namePrefix or [ (if useCoq then "coq" else "rocq") ];
+  append-version =
+    p: n:
+    let
+      version = if n == "rocq" then rocqPackages.rocq-core.version else rocqPackages.${n}.version;
+    in
+    p + display-pkg n "" version + "-";
+  prefix-name = foldl append-version "" namePrefix;
+  opam-name = args.opam-name or (concatStringsSep "-" (namePrefix ++ [ pname ]));
   rocq-core = if useCoq then coq // { rocq-version = coq.coq-version; } else args0.rocq-core;
   rocqlib-flags = [
     "COQLIBINSTALL=$(out)/lib/coq/${rocq-core.rocq-version}/user-contrib"
diff --git a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
index c40340feeb35..3941139e8770 100644
--- a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
@@ -85,7 +85,7 @@ let
           ;
 
         namePrefix = [
-          "rocq-core"
+          "rocq"
           "mathcomp"
         ];
 
diff --git a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
index 2643fdda7456..71f3ca0c6be2 100644
--- a/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-bigenough/default.nix
@@ -9,7 +9,7 @@
 mkRocqDerivation {
 
   namePrefix = [
-    "rocq-core"
+    "rocq"
     "mathcomp"
   ];
   pname = "bigenough";
diff --git a/pkgs/development/rocq-modules/mathcomp-finmap/default.nix b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
index 5fd9b61f82e4..8e5ed395218d 100644
--- a/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-finmap/default.nix
@@ -9,7 +9,7 @@
 mkRocqDerivation {
 
   namePrefix = [
-    "rocq-core"
+    "rocq"
     "mathcomp"
   ];
   pname = "finmap";
diff --git a/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix
index e260b8308d0b..8a8fa9c78a2c 100644
--- a/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-real-closed/default.nix
@@ -10,7 +10,7 @@
 mkRocqDerivation {
 
   namePrefix = [
-    "rocq-core"
+    "rocq"
     "mathcomp"
   ];
   pname = "real-closed";