rocqPackages.mathcomp-bigenough: init at 1.0.4

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

@@ -6,37 +6,47 @@
   version ? null,
 }:
 
-mkCoqDerivation {
+let
+  derivation = mkCoqDerivation {
 
-  namePrefix = [
-    "coq"
-    "mathcomp"
-  ];
-  pname = "bigenough";
-  owner = "math-comp";
+    namePrefix = [
+      "coq"
+      "mathcomp"
+    ];
+    pname = "bigenough";
+    owner = "math-comp";
 
-  release = {
-    "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
-    "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
-    "1.0.2".sha256 = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
-    "1.0.3".sha256 = "sha256-9ObUoaavnninL72r5iqkLz7lJBpcKXXi8LXKGhgx/N4=";
+    release = {
+      "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
+      "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
+      "1.0.2".sha256 = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
+      "1.0.3".sha256 = "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;
+    };
   };
-  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

pkgs/development/rocq-modules/mathcomp-bigenough/default.nix

@@ -0,0 +1,37 @@
+{
+  rocq-core,
+  mkRocqDerivation,
+  mathcomp-boot,
+  lib,
+  version ? null,
+}:
+
+mkRocqDerivation {
+
+  namePrefix = [
+    "rocq-core"
+    "mathcomp"
+  ];
+  pname = "bigenough";
+  owner = "math-comp";
+
+  release = {
+    "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.1") "1.0.4")
+    ] null;
+
+  propagatedBuildInputs = [ mathcomp-boot ];
+
+  meta = {
+    description = "Small library to do epsilon - N reasonning";
+    license = lib.licenses.cecill-b;
+  };
+}

pkgs/top-level/rocq-packages.nix

@@ -46,6 +46,7 @@ let
       mathcomp-solvable = self.mathcomp.solvable;
       mathcomp-field = self.mathcomp.field;
       mathcomp-character = self.mathcomp.character;
+      mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { };
       parseque = callPackage ../development/rocq-modules/parseque { };
       relation-algebra = callPackage ../development/rocq-modules/relation-algebra { };
       rocq-elpi = callPackage ../development/rocq-modules/rocq-elpi { };