coqPackages.metarocq: 1.4.1 -> 1.5.1 (#498952)

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

@@ -3,7 +3,7 @@
   mkCoqDerivation,
   which,
   coq,
-  metarocq,
+  metarocq-erasure,
   bignums,
   QuickChick,
   stdpp,
@@ -25,14 +25,15 @@ mkCoqDerivation {
     in
 
     lib.switch coq.coq-version [
-      (case "9.1" "1.0.0")
+      (case "9.1" "1.0.1")
     ] null;
+  release."1.0.1".sha256 = "sha256-HqbgUnGcZHkeG6qLf4qp/JT5oTPmdfOn1IJqnrloM2U=";
   release."1.0.0".sha256 = "sha256-R+kWOZtR7T2LVQnHmLGDmGpLO0S76fPRWJpsO9nWqLE=";
   releaseRev = v: "v${v}";
 
   propagatedBuildInputs = [
     coq.ocamlPackages.findlib
-    metarocq
+    metarocq-erasure
     bignums
     QuickChick
     stdpp

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

@@ -4,7 +4,7 @@
   which,
   coq,
   stdlib,
-  metarocq,
+  metarocq-erasure,
   version ? null,
   single ? false,
 }:
@@ -29,13 +29,15 @@ let
     lib.switch
       [
         coq.coq-version
-        metarocq.version
+        metarocq-erasure.version
       ]
       [
+        (case "9.1" "1.5.1-9.1" "0.2.1")
         (case "9.1" (lib.versions.range "1.4" "1.4.1") "0.2.0")
       ]
       null;
   release = {
+    "0.2.1".sha256 = "sha256-GWdu/l7CipeBubgS5OGHsZfpP2Fkr1cfiZMRH5d1n0g=";
     "0.2.0".sha256 = "sha256-rgg39X45IXjcnejBhh8N7wMiH+gHQrfO8pBbFEWOGVI=";
   };
   releaseRev = v: "v${v}";
@@ -87,7 +89,7 @@ let
             propagatedBuildInputs = [
               stdlib
               coq.ocamlPackages.findlib
-              metarocq
+              metarocq-erasure
             ]
             ++ typedextraction-deps;
 

pkgs/development/coq-modules/ceres-bs/default.nix

@@ -2,7 +2,7 @@
   lib,
   mkCoqDerivation,
   coq,
-  metarocq,
+  metarocq-utils,
   stdlib,
   version ? null,
 }:
@@ -31,7 +31,7 @@ mkCoqDerivation {
   propagatedBuildInputs = [
     coq.ocamlPackages.findlib
     stdlib
-    metarocq
+    metarocq-utils
   ];
 
   meta = {

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

@@ -4,6 +4,8 @@
   single ? false,
   coq,
   equations,
+  ExtLib,
+  stdlib,
   version ? null,
 }@args:
 
@@ -15,7 +17,7 @@ let
       case = case: out: { inherit case out; };
     in
     lib.switch coq.coq-version [
-      (case "9.1" "1.4.1-9.1")
+      (case "9.1" "1.5.1-9.1")
       (case "9.0" "1.4-9.0.1")
     ] null;
   release = {
@@ -23,6 +25,7 @@ let
     "1.4-9.0.1".sha256 = "sha256-zMUd2A6EG0LYK3L9ABQvS/Et4MDpSmf3Pxd9+IPNYkI=";
     "1.4-9.1".sha256 = "sha256-v6jFvUavIzyb/e6ytAaZjxQLFM9uW9TDUB77yRO74eE=";
     "1.4.1-9.1".sha256 = "sha256-tzoAWX74lg7pArGVP11QBvDRKMvmGxXvrf3+1E3Y4DI=";
+    "1.5.1-9.1".sha256 = "sha256-0iFnSzfbufn2XhJ8EPyWu3KIiHYwxfMVQa2KT6GSR7s=";
   };
   releaseRev = v: "v${v}";
 
@@ -91,6 +94,8 @@ let
           mlPlugin = true;
           propagatedBuildInputs = [
             equations
+            ExtLib
+            stdlib
             coq.ocamlPackages.zarith
             coq.ocamlPackages.stdlib-shims
           ]