diff --git a/pkgs/development/coq-modules/LibHyps/default.nix b/pkgs/development/coq-modules/LibHyps/default.nix
index b0997e857b09..ffdc98f75bc7 100644
--- a/pkgs/development/coq-modules/LibHyps/default.nix
+++ b/pkgs/development/coq-modules/LibHyps/default.nix
@@ -4,7 +4,7 @@ mkCoqDerivation {
   pname = "LibHyps";
   owner = "Matafou";
   inherit version;
-  defaultVersion = if (lib.versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
+  defaultVersion = if (lib.versions.range "8.11" "8.17") coq.version then "2.0.4.1" else null;
   release = {
     "2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h";
   };
diff --git a/pkgs/development/coq-modules/addition-chains/default.nix b/pkgs/development/coq-modules/addition-chains/default.nix
index f40bdbf1899c..411a52f9ca46 100644
--- a/pkgs/development/coq-modules/addition-chains/default.nix
+++ b/pkgs/development/coq-modules/addition-chains/default.nix
@@ -12,7 +12,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.13" "8.16"; out = "0.6"; }
+    { case = range "8.13" "8.17"; out = "0.6"; }
     { case = range "8.11" "8.12"; out = "0.4"; }
   ] null;
 
diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix
index ed214533b03f..dc0bd6cfcadc 100644
--- a/pkgs/development/coq-modules/category-theory/default.nix
+++ b/pkgs/development/coq-modules/category-theory/default.nix
@@ -17,7 +17,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.14" "8.16"; out = "1.0.0"; }
+    { case = range "8.14" "8.17"; out = "1.0.0"; }
     { case = range "8.10" "8.15"; out = "20211213"; }
     { case = range "8.8" "8.9"; out = "20190414"; }
     { case = range "8.6" "8.7"; out = "20180709"; }
diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/coq-modules/coq-record-update/default.nix
index a0b27dda845f..3bf079f3a98f 100644
--- a/pkgs/development/coq-modules/coq-record-update/default.nix
+++ b/pkgs/development/coq-modules/coq-record-update/default.nix
@@ -5,7 +5,7 @@
   owner = "tchajed";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.10" "8.16";  out = "0.3.1"; }
+    { case = range "8.10" "8.17";  out = "0.3.1"; }
   ] null;
   release."0.3.1".sha256 = "sha256-DyGxO2tqmYZZluXN6Oy5Tw6fuLMyuyxonj8CCToWKkk=";
   release."0.3.0".sha256 = "1ffr21dd6hy19gxnvcd4if2450iksvglvkd6q5713fajd72hmc0z";
diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix
index 82d2a16f77ff..e0197db71b94 100644
--- a/pkgs/development/coq-modules/metalib/default.nix
+++ b/pkgs/development/coq-modules/metalib/default.nix
@@ -5,7 +5,7 @@ mkCoqDerivation {
   owner = "plclub";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.14" "8.16"; out = "8.15"; }
+    { case = range "8.14" "8.17"; out = "8.15"; }
     { case = range "8.10" "8.13"; out = "8.10"; }
   ] null;
   releaseRev = v: "coq${v}";
diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix
index 468be219d0d7..9ed22266bec6 100644
--- a/pkgs/development/coq-modules/semantics/default.nix
+++ b/pkgs/development/coq-modules/semantics/default.nix
@@ -15,7 +15,7 @@ mkCoqDerivation rec {
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.10" "8.16"; out = "8.14.0"; }
+    { case = range "8.10" "8.17"; out = "8.14.0"; }
     { case = "8.9"; out = "8.9.0"; }
     { case = "8.8"; out = "8.8.0"; }
     { case = "8.7"; out = "8.7.0"; }
diff --git a/pkgs/development/coq-modules/trakt/default.nix b/pkgs/development/coq-modules/trakt/default.nix
index 8bc7581489c3..ba66c4f86efc 100644
--- a/pkgs/development/coq-modules/trakt/default.nix
+++ b/pkgs/development/coq-modules/trakt/default.nix
@@ -9,7 +9,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with lib.versions; lib.switch [ coq.version ] [
-    { cases = [ (range "8.13" "8.16") ]; out = "1.0"; }
+    { cases = [ (range "8.13" "8.17") ]; out = "1.0"; }
   ] null;
 
   propagatedBuildInputs = [ coq-elpi ];
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 256874b9833c..c8ab05a72910 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -14507,7 +14507,7 @@ with pkgs;
 
   comby = callPackage ../development/tools/comby { };
 
-  inherit (coqPackages) compcert;
+  inherit (coqPackages_8_16) compcert;
 
   computecpp-unwrapped = callPackage ../development/compilers/computecpp { };
   computecpp = wrapCCWith rec {
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index ca25f9beef52..f8e249b7bbbd 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -183,7 +183,7 @@ in rec {
   coqPackages_8_15 = mkCoqPackages coq_8_15;
   coqPackages_8_16 = mkCoqPackages coq_8_16;
   coqPackages_8_17 = mkCoqPackages coq_8_17;
-  coqPackages = recurseIntoAttrs coqPackages_8_16;
+  coqPackages = recurseIntoAttrs coqPackages_8_17;
   coq = coqPackages.coq;
 
 }