Rocq 9.1

Author: 4ever2

.github/workflows/nix-action-default.yml

@@ -327,4 +327,4 @@ on:
   push:
     branches:
     - master
-    - rocq-9.0
+    - rocq-9.1

.nix/config.nix

@@ -33,7 +33,7 @@ with (import <nixpkgs> {}).lib;
   ##     should be preferred then.
   buildInputs = [ "equations" "metarocq" ];
   nativeBuildInputs = [ "equations" ];
-    
+
   ## Indicate the relative location of your _CoqProject
   ## If not specified, it defaults to "_CoqProject"
   # coqproject = "_CoqProject";
@@ -49,14 +49,14 @@ with (import <nixpkgs> {}).lib;
   bundles.default = {
     ## You can override Rocq and other Rocq rocqPackages
     ## through the following attribute
-    rocqPackages.rocq-core.override.version = "9.0";
-    rocqPackages.coq-core.override.version = "9.0";
+    rocqPackages.rocq-core.override.version = "9.1";
+    rocqPackages.coq-core.override.version = "9.1";
     ## You can override Coq and other Coq coqPackages
     ## through the following attribute
-    coqPackages.coq.override.version = "9.0";
-    coqPackages.equations.override.version = "1.3.1-9.0";
-    
-    coqPackages.metarocq.override.version = "1.4-9.0";
+    coqPackages.coq.override.version = "9.1";
+    coqPackages.equations.override.version = "1.3.1-9.1";
+
+    coqPackages.metarocq.override.version = "1.4.1-9.1";
     coqPackages.ceres.override.version = "0.4.1";
 
     ## In some cases, light overrides are not available/enough
@@ -104,17 +104,17 @@ with (import <nixpkgs> {}).lib;
   cachix.coq = {};
   cachix.math-comp = {};
   cachix.coq-community = {};
-  
+
   ## If you have write access to one of these caches you can
   ## provide the auth token or signing key through a secret
   ## variable on GitHub. Then, you should give the variable
   ## name here. For instance, coq-community projects can use
   ## the following line instead of the one above:
   cachix.metarocq.authToken = "CACHIX_AUTH_TOKEN";
-  
+
   ## Or if you have a signing key for a given Cachix cache:
   # cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
-  
+
   ## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
   ## are the names of secret variables. They are set in
   ## GitHub's web interface.

rocq-verified-extraction.opam

@@ -16,15 +16,15 @@ install: [
   [make "-j%{jobs}%" "install"]
 ]
 depends: [
-  "rocq-core" { >= "9.0" }
+  "rocq-core" { >= "9.1" }
   "rocq-stdlib" { >= "9.0" }
   "coq-ceres" { >= "0.4.1"}
-  "rocq-metarocq-erasure-plugin" { = "1.4+9.0" }
+  "rocq-metarocq-erasure-plugin" { >= "1.4" & < "1.4.2" }
   "malfunction" { >= "0.7" }
 ]
 tags: [
   "keyword:extraction"
   "category:Miscellaneous/Rocq Extensions"
   "date:2025-04-23"
   "logpath:VerifiedExtraction"
-]
+]