coqPackages.mathcomp*: update stdlib dependencies

pkgs/development/coq-modules/fourcolor/default.nix

···
   mkCoqDerivation,
   coq,
   mathcomp,
-  stdlib,
   version ? null,
 }:
 
···
     mathcomp.algebra
     mathcomp.ssreflect
     mathcomp.fingroup
-    stdlib
   ];
 
   meta = with lib; {

pkgs/development/coq-modules/hierarchy-builder/default.nix

···
    else
    { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; })
   //
-  lib.optionalAttrs (lib.versions.isLe "1.8.1" o.version)
+  lib.optionalAttrs (o.version != null && o.version == "1.8.1")
     { propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ]; }
 )

pkgs/development/coq-modules/jasmin/default.nix

···
   mkCoqDerivation,
   coq,
   mathcomp,
+  mathcomp-algebra-tactics,
   mathcomp-word,
   version ? null,
 }:
···
   release."2024.07.2".sha256 = "sha256-aF8SYY5jRxQ6iEr7t6mRN3BEmIDhJ53PGhuZiJGB+i8=";
 
   propagatedBuildInputs = [
+    mathcomp-algebra-tactics
     mathcomp-word
   ];
 

pkgs/development/coq-modules/mathcomp-analysis/default.nix

···
   mathcomp-finmap,
   mathcomp-bigenough,
   hierarchy-builder,
+  stdlib,
   single ? false,
   coqPackages,
   coq,
···
       ];
       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";
-        }
+        { 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 ({
···
           ++ lib.optionals (lib.elem package [
             "analysis"
             "single"
-          ]) analysis-deps;
+          ]) analysis-deps
+          ++ lib.optional (lib.elem package [
+            "reals-stdlib"
+            "analysis-stdlib"
+            "single"
+          ]) stdlib;
 
         preBuild = ''
           cd ${pkgpath}

pkgs/development/coq-modules/mathcomp-finmap/default.nix

···
   coq,
   mkCoqDerivation,
   mathcomp,
-  stdlib,
   lib,
   version ? null,
 }:
···
     "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
   };
 
-  propagatedBuildInputs = [ mathcomp.ssreflect stdlib ];
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
 
   meta = {
     description = "Finset and finmap library";

pkgs/development/coq-modules/mathcomp-real-closed/default.nix

···
   mkCoqDerivation,
   mathcomp,
   mathcomp-bigenough,
-  stdlib,
   lib,
   version ? null,
 }:
···
     mathcomp.fingroup
     mathcomp.solvable
     mathcomp-bigenough
-    stdlib
   ];
 
   meta = {

pkgs/development/coq-modules/mathcomp-tarjan/default.nix

···
   mkCoqDerivation,
   mathcomp-ssreflect,
   mathcomp-fingroup,
-  stdlib,
   lib,
   version ? null,
 }@args:
···
   propagatedBuildInputs = [
     mathcomp-ssreflect
     mathcomp-fingroup
-    stdlib
   ];
 
   meta = {

pkgs/development/coq-modules/mathcomp-word/default.nix

···
   coq,
   mkCoqDerivation,
   mathcomp,
+  stdlib,
   lib,
   version ? null,
 }:
···
     mathcomp.algebra
     mathcomp.ssreflect
     mathcomp.fingroup
+    stdlib
   ];
 
   meta = with lib; {

pkgs/development/coq-modules/mathcomp/default.nix

···
         mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
         nativeBuildInputs = lib.optionals withDoc [ graphviz lua ];
         buildInputs = [ ncurses ];
-        propagatedBuildInputs = [ stdlib ] ++ mathcomp-deps;
+        propagatedBuildInputs = mathcomp-deps;
 
         buildFlags = lib.optional withDoc "doc";
 
···
       }
     );
     patched-derivation4 = patched-derivation3.overrideAttrs (o:
-      lib.optionalAttrs (o.version != null
-        && lib.versions.isLe "2.3.0" o.version)
+      lib.optionalAttrs (o.version != null && o.version == "2.3.0")
       {
         propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
       }

pkgs/development/coq-modules/odd-order/default.nix

···
   lib,
   mkCoqDerivation,
   mathcomp,
-  stdlib,
   version ? null,
 }:
 
···
     mathcomp.solvable
     mathcomp.field
     mathcomp.all
-    stdlib
   ];
 
   meta = with lib; {