Merge pull request #212009 from Shawn8901/remove_with_lib_2

treewide: remove global with lib; statements in pkgs/coq-modules

77 files changed, 209 insertions, 242 deletions

diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/coq-modules/Cheerios/default.nix
index 7ded64ec572..5a7ec31f50c 100644
--- a/pkgs/development/coq-modules/Cheerios/default.nix
+++ b/pkgs/development/coq-modules/Cheerios/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, StructTact, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname   = "cheerios";
   owner   = "uwplse";
   inherit version;
-  defaultVersion = if versions.range "8.6" "8.16" coq.version then "20200201" else null;
+  defaultVersion = if lib.versions.range "8.6" "8.16" coq.version then "20200201" else null;
   release."20200201".rev    = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";
   release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";
 
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix
index 9dabae0bdbc..a926f6d8092 100644
--- a/pkgs/development/coq-modules/CoLoR/default.nix
+++ b/pkgs/development/coq-modules/CoLoR/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, bignums, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "color";
   owner = "fblanqui";
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     {case = range "8.12" "8.16"; out = "1.8.2"; }
     {case = range "8.10" "8.11"; out = "1.7.0"; }
     {case = range "8.8"  "8.9";  out = "1.6.0"; }
@@ -26,6 +26,6 @@ with lib; mkCoqDerivation {
   meta = {
     homepage = "https://github.com/fblanqui/color";
     description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant.";
-    maintainers = with maintainers; [ jpas jwiegley ];
+    maintainers = with lib.maintainers; [ jpas jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix
index 7b9ded1e399..a0761dfb519 100644
--- a/pkgs/development/coq-modules/HoTT/default.nix
+++ b/pkgs/development/coq-modules/HoTT/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "HoTT";
   repo = "Coq-HoTT";
   owner = "HoTT";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.14" "8.16"; out = coq.coq-version; }
   ] null;
   releaseRev = v: "V${v}";
@@ -20,6 +20,6 @@ with lib; mkCoqDerivation {
   meta = {
     homepage = "https://homotopytypetheory.org/";
     description = "Homotopy type theory";
-    maintainers = with maintainers; [ siddharthist ];
+    maintainers = with lib.maintainers; [ siddharthist ];
   };
 }
diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/coq-modules/ITree/default.nix
index 23922dcce42..e0a9e1f6bfc 100644
--- a/pkgs/development/coq-modules/ITree/default.nix
+++ b/pkgs/development/coq-modules/ITree/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "InteractionTrees";
   owner = "DeepSpec";
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     { case = range "8.10" "8.16";  out = "4.0.0"; }
   ] null;
   release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
@@ -12,6 +12,6 @@ with lib; mkCoqDerivation rec {
   propagatedBuildInputs = [ coq-ext-lib paco ];
   meta = {
     description = "A Library for Representing Recursive and Impure Programs in Coq";
-    maintainers = with maintainers; [ larsr ];
+    maintainers = with lib.maintainers; [ larsr ];
   };
 }
diff --git a/pkgs/development/coq-modules/LibHyps/default.nix b/pkgs/development/coq-modules/LibHyps/default.nix
index 1a9eb9cec05..b0997e857b0 100644
--- a/pkgs/development/coq-modules/LibHyps/default.nix
+++ b/pkgs/development/coq-modules/LibHyps/default.nix
@@ -1,11 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib;
 mkCoqDerivation {
   pname = "LibHyps";
   owner = "Matafou";
   inherit version;
-  defaultVersion = if (versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
+  defaultVersion = if (lib.versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
   release = {
     "2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h";
   };
@@ -16,6 +15,6 @@ mkCoqDerivation {
 
   meta = {
     description = "Hypotheses manipulation library";
-    license = licenses.mit;
+    license = lib.licenses.mit;
   };
 }
diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/coq-modules/StructTact/default.nix
index 3fb8a42cfb5..778ab142654 100644
--- a/pkgs/development/coq-modules/StructTact/default.nix
+++ b/pkgs/development/coq-modules/StructTact/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "StructTact";
   owner = "uwplse";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.6" "8.16"; out = "20210328"; }
     { case = range "8.5" "8.13"; out = "20181102"; }
   ] null;
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
index 8a4243a8704..72d88dec6f1 100644
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@@ -1,7 +1,5 @@
 { lib, mkCoqDerivation, coq, compcert, ITree, version ? null }:
 
-with lib;
-
 # A few modules that are not built and installed by default
 #  but that may be useful to some users.
 # They depend on ITree.
@@ -11,7 +9,7 @@ let extra_floyd_files = [
   "powerlater.v"
   ]
   # floyd/printf.v is broken in VST 2.9
-  ++ optional (!versions.isGe "8.13" coq.coq-version) "printf.v"
+  ++ lib.optional (!lib.versions.isGe "8.13" coq.coq-version) "printf.v"
   ++ [
   "quickprogram.v"
   ];
@@ -24,7 +22,7 @@ mkCoqDerivation {
   owner = "PrincetonUniversity";
   repo = "VST";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.15" "8.16"; out = "2.11.1"; }
     { case = range "8.14" "8.16"; out = "2.10"; }
     { case = range "8.13" "8.15"; out = "2.9"; }
diff --git a/pkgs/development/coq-modules/Velisarios/default.nix b/pkgs/development/coq-modules/Velisarios/default.nix
index 08322fb7fc4..62eb9c389ab 100644
--- a/pkgs/development/coq-modules/Velisarios/default.nix
+++ b/pkgs/development/coq-modules/Velisarios/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "Velisarios";
   owner = "vrahli";
   inherit version;
-  defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
+  defaultVersion = if lib.versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
 
   release."20180221".rev    = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
   release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
diff --git a/pkgs/development/coq-modules/Verdi/default.nix b/pkgs/development/coq-modules/Verdi/default.nix
index 80b964b3904..6dec34a095d 100644
--- a/pkgs/development/coq-modules/Verdi/default.nix
+++ b/pkgs/development/coq-modules/Verdi/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }:
 
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "verdi";
   owner = "uwplse";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.7" "8.16"; out = "20211026"; }
     { case = range "8.7" "8.14"; out = "20210524"; }
     { case = range "8.7" "8.13"; out = "20200131"; }
diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix
index 90ddf3e524f..180b7b88fce 100644
--- a/pkgs/development/coq-modules/aac-tactics/default.nix
+++ b/pkgs/development/coq-modules/aac-tactics/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "aac-tactics";
@@ -21,7 +20,7 @@ mkCoqDerivation {
   release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = "8.16"; out = "8.16.0"; }
     { case = "8.15"; out = "8.15.1"; }
     { case = "8.14"; out = "8.14.1"; }
@@ -37,7 +36,7 @@ mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     description = "Coq plugin providing tactics for rewriting universally quantified equations";
     longDescription = ''
       This Coq plugin provides tactics for rewriting universally quantified
diff --git a/pkgs/development/coq-modules/addition-chains/default.nix b/pkgs/development/coq-modules/addition-chains/default.nix
index 63ba0e80507..f40bdbf1899 100644
--- a/pkgs/development/coq-modules/addition-chains/default.nix
+++ b/pkgs/development/coq-modules/addition-chains/default.nix
@@ -1,6 +1,5 @@
 { lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, mathcomp-fingroup, paramcoq
 , version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "addition-chains";
@@ -12,7 +11,7 @@ mkCoqDerivation {
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.13" "8.16"; out = "0.6"; }
     { case = range "8.11" "8.12"; out = "0.4"; }
   ] null;
@@ -21,7 +20,7 @@ mkCoqDerivation {
 
   useDune = true;
 
-  meta = {
+  meta = with lib; {
     description = "Exponentiation algorithms following addition chains";
     longDescription = ''
       Addition chains are algorithms for computations of the p-th
diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix
index 5a7331c2220..72768777c1b 100644
--- a/pkgs/development/coq-modules/autosubst/default.nix
+++ b/pkgs/development/coq-modules/autosubst/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "autosubst";
@@ -8,13 +7,13 @@ mkCoqDerivation {
   release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "1.7"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp-ssreflect ];
 
-  meta = {
+  meta = with lib; {
     homepage = "https://www.ps.uni-saarland.de/autosubst/";
     description = "Automation for de Bruijn syntax and substitution in Coq";
     maintainers = with maintainers; [ siraben jwiegley ];
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index f2e64ab2f61..c62e20a5a2e 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "bignums";
   owner = "coq";
   displayVersion = { bignums = ""; };
   inherit version;
-  defaultVersion = if versions.isGe "8.6" coq.coq-version
+  defaultVersion = if lib.versions.isGe "8.6" coq.coq-version
     then "${coq.coq-version}.0" else null;
 
   release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
@@ -25,5 +25,5 @@ with lib; mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = { license = licenses.lgpl2; };
+  meta = { license = lib.licenses.lgpl2; };
 }
diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix
index 97feac90c3b..ed214533b03 100644
--- a/pkgs/development/coq-modules/category-theory/default.nix
+++ b/pkgs/development/coq-modules/category-theory/default.nix
@@ -1,6 +1,6 @@
 { lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   pname = "category-theory";
   owner = "jwiegley";
@@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
   release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.14" "8.16"; out = "1.0.0"; }
     { case = range "8.10" "8.15"; out = "20211213"; }
     { case = range "8.8" "8.9"; out = "20190414"; }
@@ -28,6 +28,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "A formalization of category theory in Coq for personal study and practical work";
-    maintainers = with maintainers; [ jwiegley ];
+    maintainers = with lib.maintainers; [ jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/ceres/default.nix b/pkgs/development/coq-modules/ceres/default.nix
index 375eb6c75bb..75d57936ff5 100644
--- a/pkgs/development/coq-modules/ceres/default.nix
+++ b/pkgs/development/coq-modules/ceres/default.nix
@@ -1,6 +1,5 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib;
 mkCoqDerivation {
 
   pname = "ceres";
@@ -8,10 +7,10 @@ mkCoqDerivation {
   owner = "Lysxia";
 
   inherit version;
-  defaultVersion = if versions.range "8.8" "8.16" coq.version then "0.4.0" else null;
+  defaultVersion = if lib.versions.range "8.8" "8.16" coq.version then "0.4.0" else null;
   release."0.4.0".sha256 = "sha256:0zwp3pn6fdj0qdig734zdczrls886al06mxqhhabms0jvvqijmbi";
 
-  meta = {
+  meta = with lib; {
     description = "Library for serialization to S-expressions";
     license = licenses.mit;
     maintainers = with maintainers; [ Zimmi48 ];
diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index fb6527989d8..fb33f92bcc2 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -5,8 +5,6 @@
 , version ? null
 }:
 
-with lib;
-
 let compcert = mkCoqDerivation rec {
 
   pname = "compcert";
@@ -15,7 +13,7 @@ let compcert = mkCoqDerivation rec {
   inherit version;
   releaseRev = v: "v${v}";
 
-  defaultVersion =  with versions; switch coq.version [
+  defaultVersion =  with lib.versions; lib.switch coq.version [
       { case = range "8.14" "8.16"; out = "3.11"; }
       { case = isEq "8.13"        ; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
@@ -84,7 +82,7 @@ let compcert = mkCoqDerivation rec {
 }; in
 compcert.overrideAttrs (o:
   {
-    patches = with versions; switch [ coq.version o.version ] [
+    patches = with lib.versions; lib.switch [ coq.version o.version ] [
       { cases = [ (range "8.12.2" "8.13.2") "3.8" ];
         out = [
           # Support for Coq 8.12.2
diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix
index cb6dedca355..2d10f683cc3 100644
--- a/pkgs/development/coq-modules/contribs/default.nix
+++ b/pkgs/development/coq-modules/contribs/default.nix
@@ -1,16 +1,16 @@
 { lib, mkCoqDerivation, coq, callPackage }:
 
-with lib; let mkContrib = pname: coqs: param:
+  let mkContrib = pname: coqs: param:
   let contribVersion = {version ? null}: mkCoqDerivation ({
       inherit pname version;
       owner = "coq-contribs";
       mlPlugin = true;
-    } // optionalAttrs (builtins.elem coq.coq-version coqs) ({
+    } // lib.optionalAttrs (builtins.elem coq.coq-version coqs) ({
       defaultVersion = param.version;
       release = { "${param.version}" = { inherit (param) rev sha256; }; };
     } // (removeAttrs param [ "version" "rev" "sha256" ]))
   ); in
-  makeOverridable contribVersion {} ; in
+  lib.makeOverridable contribVersion {} ; in
 {
   aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] {
     "8.7" = {
diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix
index a2ef7e09a7d..16a26d9fa32 100644
--- a/pkgs/development/coq-modules/coq-bits/default.nix
+++ b/pkgs/development/coq-modules/coq-bits/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "coq-bits";
   repo = "bits";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "1.1.0"; }
     { case = range "8.7"  "8.15"; out = "1.0.0"; }
   ] null;
@@ -14,7 +14,7 @@ with lib; mkCoqDerivation {
 
   propagatedBuildInputs = [ mathcomp-algebra ];
 
-  meta = {
+  meta = with lib; {
     description = "A formalization of bitset operations in Coq";
     license = licenses.asl20;
     maintainers = with maintainers; [ ptival ];
diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix
index b6f124b3f0f..d555e55389b 100644
--- a/pkgs/development/coq-modules/coq-ext-lib/default.nix
+++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "coq-ext-lib";
   owner = "coq-ext-lib";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.11" "8.16"; out = "0.11.7"; }
     { case = range "8.8" "8.16"; out = "0.11.6"; }
     { case = range "8.8" "8.14"; out = "0.11.4"; }
@@ -30,6 +30,6 @@ with lib; mkCoqDerivation rec {
 
   meta = {
     description = "A collection of theories and plugins that may be useful in other Coq developments";
-    maintainers = with maintainers; [ jwiegley ptival ];
+    maintainers = with lib.maintainers; [ jwiegley ptival ];
   };
 }
diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/coq-modules/coq-haskell/default.nix
index 7caf754ae50..028b4c5025e 100644
--- a/pkgs/development/coq-modules/coq-haskell/default.nix
+++ b/pkgs/development/coq-modules/coq-haskell/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, ssreflect, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   pname = "coq-haskell";
   owner = "jwiegley";
   inherit version;
-  defaultVersion = if versions.range "8.5" "8.8" coq.coq-version then "20171215" else null;
+  defaultVersion = if lib.versions.range "8.5" "8.8" coq.coq-version then "20171215" else null;
   release."20171215".rev    = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
   release."20171215".sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
 
@@ -16,6 +16,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "A library for formalizing Haskell types and functions in Coq";
-    maintainers = with maintainers; [ jwiegley ];
+    maintainers = with lib.maintainers; [ jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/coq-modules/coq-record-update/default.nix
index 77c42fb48d4..a0b27dda845 100644
--- a/pkgs/development/coq-modules/coq-record-update/default.nix
+++ b/pkgs/development/coq-modules/coq-record-update/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation rec {
+ mkCoqDerivation rec {
   pname = "coq-record-update";
   owner = "tchajed";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16";  out = "0.3.1"; }
   ] null;
   release."0.3.1".sha256 = "sha256-DyGxO2tqmYZZluXN6Oy5Tw6fuLMyuyxonj8CCToWKkk=";
@@ -13,6 +13,6 @@ with lib; mkCoqDerivation rec {
   buildFlags = [ "NO_TEST=1" ];
   meta = {
     description = "Library to create Coq record update functions";
-    maintainers = with maintainers; [ ineol ];
+    maintainers = with lib.maintainers; [ ineol ];
   };
 }
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index d3a8e366a0a..1ccbf9e82a0 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -2,14 +2,12 @@
   mathcomp-real-closed,
   lib, version ? null }:
 
-with lib;
-
 (mkCoqDerivation {
 
   pname = "CoqEAL";
 
   inherit version;
-  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
       { cases = [ (range "8.13" "8.16") (isGe "1.13.0") ]; out = "1.1.1"; }
       { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.1.0"; }
       { cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; }
@@ -28,9 +26,9 @@ with lib;
 
   meta = {
     description = "CoqEAL - The Coq Effective Algebra Library";
-    license = licenses.mit;
+    license = lib.licenses.mit;
   };
 }).overrideAttrs (o: {
   propagatedBuildInputs = o.propagatedBuildInputs
-  ++ optional (versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
+  ++ lib.optional (lib.versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
 })
diff --git a/pkgs/development/coq-modules/coqhammer/default.nix b/pkgs/development/coq-modules/coqhammer/default.nix
index 853e77990b6..e5e23247f14 100644
--- a/pkgs/development/coq-modules/coqhammer/default.nix
+++ b/pkgs/development/coq-modules/coqhammer/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   inherit version;
   pname = "coqhammer";
   owner = "lukaszcz";
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = "8.15"; out = "1.3.2-coq8.15"; }
     { case = "8.14"; out = "1.3.2-coq8.14"; }
     { case = "8.13"; out = "1.3.2-coq8.13"; }
@@ -57,7 +57,7 @@ with lib; mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/";
     description = "Automation for Dependent Type Theory";
     license = licenses.lgpl21;
diff --git a/pkgs/development/coq-modules/coqide/default.nix b/pkgs/development/coq-modules/coqide/default.nix
index 4e1f9e5f666..a11bfb2c0db 100644
--- a/pkgs/development/coq-modules/coqide/default.nix
+++ b/pkgs/development/coq-modules/coqide/default.nix
@@ -8,14 +8,14 @@
 , coq
 , version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "coqide";
   inherit version;
 
   inherit (coq) src;
   release."${coq.version}" = {};
 
-  defaultVersion = if versions.isGe "8.14" coq.version then coq.version else null;
+  defaultVersion = if lib.versions.isGe "8.14" coq.version then coq.version else null;
 
   preConfigure = ''
     patchShebangs dev/tools/
diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/coq-modules/coqprime/default.nix
index ac05af58725..cfba685e35f 100644
--- a/pkgs/development/coq-modules/coqprime/default.nix
+++ b/pkgs/development/coq-modules/coqprime/default.nix
@@ -1,11 +1,11 @@
 { which, lib, mkCoqDerivation, coq, bignums, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   pname = "coqprime";
   owner = "thery";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.12" "8.16"; out = "8.15"; }
     { case = range "8.10" "8.11"; out = "8.10"; }
     { case = range "8.8"  "8.9";  out = "8.8"; }
diff --git a/pkgs/development/coq-modules/coqtail-math/default.nix b/pkgs/development/coq-modules/coqtail-math/default.nix
index a4f7ca405f7..b43cadb918e 100644
--- a/pkgs/development/coq-modules/coqtail-math/default.nix
+++ b/pkgs/development/coq-modules/coqtail-math/default.nix
@@ -1,12 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib;
-
 mkCoqDerivation {
   pname = "coqtail-math";
   owner = "coq-community";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.11" "8.15"; out = "8.14"; }
     { case = range "8.11" "8.13"; out = "20201124"; }
   ] null;
@@ -15,7 +13,7 @@ mkCoqDerivation {
   release."20201124".rev    = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
   release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
   mlPlugin = true;
-  meta = {
+  meta = with lib; {
     license = licenses.lgpl3Only;
     maintainers = [ maintainers.siraben ];
   };
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index 09327f2ff76..b6e2df653be 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -1,12 +1,12 @@
 { lib, mkCoqDerivation, autoconf,
   coq, ssreflect, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "coquelicot";
   owner = "coquelicot";
   domain = "gitlab.inria.fr";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.8" "8.16"; out = "3.2.0"; }
     { case = range "8.8" "8.13"; out = "3.1.0"; }
     { case = range "8.5" "8.9";  out = "3.0.2"; }
@@ -20,7 +20,7 @@ with lib; mkCoqDerivation {
   propagatedBuildInputs = [ ssreflect ];
   useMelquiondRemake.logpath = "Coquelicot";
 
-  meta = {
+  meta =  with lib; {
     homepage = "http://coquelicot.saclay.inria.fr/";
     description = "A Coq library for Reals";
     license = licenses.lgpl3;
diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix
index d019d4b4e55..84bca53931c 100644
--- a/pkgs/development/coq-modules/corn/default.nix
+++ b/pkgs/development/coq-modules/corn/default.nix
@@ -1,9 +1,9 @@
 { lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "corn";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = "8.6"; out = "8.8.1"; }
     { case = (range "8.11" "8.16"); out = "8.16.0"; }
     { case = (range "8.7"  "8.15"); out = "8.13.0"; }
@@ -21,7 +21,7 @@ with lib; mkCoqDerivation rec {
 
   propagatedBuildInputs = [ bignums math-classes ];
 
-  meta = {
+  meta =  with lib; {
     homepage = "http://c-corn.github.io/";
     license = licenses.gpl2;
     description = "A Coq library for constructive analysis";
diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix
index f08e86ccc4f..06e80f118bc 100644
--- a/pkgs/development/coq-modules/deriving/default.nix
+++ b/pkgs/development/coq-modules/deriving/default.nix
@@ -1,14 +1,13 @@
 { lib, mkCoqDerivation, coq, version ? null
 , ssreflect
 }:
-with lib;
 
 mkCoqDerivation {
   pname = "deriving";
   owner = "arthuraa";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.11" "8.16"; out = "0.1.0"; }
   ] null;
 
@@ -20,7 +19,7 @@ mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     description = "Generic instances of MathComp classes";
     license = licenses.mit;
     maintainers = [ maintainers.vbgl ];
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix
index e2472946557..da26b0774d4 100644
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -1,14 +1,13 @@
 { lib, mkCoqDerivation, autoreconfHook, coq, version ? null }:
 
-with lib;
-let hasWarning = versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
+let hasWarning = lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
 
 mkCoqDerivation {
   pname = "dpdgraph";
   owner = "Karmaki";
   repo = "coq-dpdgraph";
   inherit version;
-  defaultVersion = switch coq.coq-version [
+  defaultVersion = lib.switch coq.coq-version [
     { case = "8.16"; out = "1.0+8.16"; }
     { case = "8.15"; out = "1.0+8.15"; }
     { case = "8.14"; out = "1.0+8.14"; }
@@ -47,11 +46,11 @@ mkCoqDerivation {
 
   # dpd_compute.ml uses deprecated Pervasives.compare
   # Versions prior to 0.6.5 do not have the WARN_ERR build flag
-  preConfigure = optionalString hasWarning ''
+  preConfigure = lib.optionalString hasWarning ''
     substituteInPlace Makefile.in --replace "-warn-error +a " ""
   '';
 
-  buildFlags = optional hasWarning "WARN_ERR=";
+  buildFlags = lib.optional hasWarning "WARN_ERR=";
 
   preInstall = ''
     mkdir -p $out/bin
@@ -59,7 +58,7 @@ mkCoqDerivation {
 
   extraInstallFlags = [ "BINDIR=$(out)/bin" ];
 
-  meta = {
+  meta = with lib; {
     description = "Build dependency graphs between Coq objects";
     license = licenses.lgpl21;
     maintainers = with maintainers; [ vbgl ];
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index ffe72ad330b..5f38c4bbae2 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; (mkCoqDerivation {
+(mkCoqDerivation {
   pname = "equations";
   owner = "mattam82";
   repo = "Coq-Equations";
   inherit version;
-  defaultVersion = switch coq.coq-version [
+  defaultVersion = lib.switch coq.coq-version [
     { case = "8.16"; out = "1.3+8.16"; }
     { case = "8.15"; out = "1.3+8.15"; }
     { case = "8.14"; out = "1.3+8.14"; }
@@ -57,11 +57,11 @@ with lib; (mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     homepage = "https://mattam82.github.io/Coq-Equations/";
     description = "A plugin for Coq to add dependent pattern-matching";
     maintainers = with maintainers; [ jwiegley ];
   };
 }).overrideAttrs (o: {
-  preBuild = "coq_makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
+  preBuild = "coq_makefile -f _CoqProject -o Makefile${lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
 })
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index 2a038ff0c11..b6345d7b0ac 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -2,14 +2,13 @@
 , ssreflect
 , deriving
 }:
-with lib;
 
 (mkCoqDerivation {
   pname = "extructures";
   owner = "arthuraa";
 
   inherit version;
-  defaultVersion = with versions; switch [coq.coq-version ssreflect.version] [
+  defaultVersion = with lib.versions; lib.switch [coq.coq-version ssreflect.version] [
     { cases = [(range "8.11" "8.16") (isGe "1.12.0") ]; out = "0.3.1"; }
     { cases = [(range "8.11" "8.14") (isLe "1.12.0") ]; out = "0.3.0"; }
     { cases = [(range "8.10" "8.12") (isLe "1.12.0") ]; out = "0.2.2"; }
@@ -23,7 +22,7 @@ with lib;
 
   propagatedBuildInputs = [ ssreflect ];
 
-  meta = {
+  meta = with lib; {
     description = "Finite data structures with extensional reasoning";
     license = licenses.mit;
     maintainers = [ maintainers.vbgl ];
@@ -31,5 +30,5 @@ with lib;
 
 }).overrideAttrs (o: {
   propagatedBuildInputs = o.propagatedBuildInputs
-  ++ optional (versionAtLeast o.version "0.3.0") deriving;
+  ++ lib.optional (lib.versionAtLeast o.version "0.3.0") deriving;
 })
diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix
index d94dc03b637..0a6375907e8 100644
--- a/pkgs/development/coq-modules/fiat/HEAD.nix
+++ b/pkgs/development/coq-modules/fiat/HEAD.nix
@@ -1,6 +1,6 @@
 {lib, mkCoqDerivation, coq, python27, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "fiat";
   owner = "mit-plv";
   repo = "fiat";
@@ -29,6 +29,6 @@ with lib; mkCoqDerivation rec {
   meta = {
     homepage = "http://plv.csail.mit.edu/fiat/";
     description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
-    maintainers = with maintainers; [ jwiegley ];
+    maintainers = with lib.maintainers; [ jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix
index ed973996fee..cf39c8211b7 100644
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@@ -1,12 +1,12 @@
 { lib, bash, autoconf, automake,
   mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "flocq";
   owner = "flocq";
   domain = "gitlab.inria.fr";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.14" "8.16"; out = "4.1.0"; }
     { case = range "8.7" "8.15"; out = "3.4.3"; }
     { case = range "8.5" "8.8"; out = "2.6.1"; }
@@ -22,7 +22,7 @@ with lib; mkCoqDerivation {
   mlPlugin = true;
   useMelquiondRemake.logpath = "Flocq";
 
-  meta = {
+  meta = with lib; {
     description = "A floating-point formalization for the Coq system";
     license = licenses.lgpl3;
     maintainers = with maintainers; [ jwiegley ];
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index 3615f5513a3..6548da52b9f 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, mathcomp, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "fourcolor";
@@ -12,15 +11,15 @@ mkCoqDerivation {
   release."1.2.5".sha256 = "sha256-3qOPNCRjGK2UdHGMSqElpIXhAPVCklpeQgZwf9AFals=";
 
   inherit version;
-  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
     { cases = [ (isGe "8.11") (isGe "1.12") ]; out = "1.2.5"; }
     { cases = [ (isGe "8.11") (range "1.11" "1.14") ]; out = "1.2.4"; }
-    { cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
+    { cases = [ (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
 
-  meta = {
+  meta =  with lib; {
     description = "Formal proof of the Four Color Theorem ";
     maintainers = with maintainers; [ siraben ];
     license = licenses.cecill-b;
diff --git a/pkgs/development/coq-modules/gaia-hydras/default.nix b/pkgs/development/coq-modules/gaia-hydras/default.nix
index 5377600caba..4f9e7a12e04 100644
--- a/pkgs/development/coq-modules/gaia-hydras/default.nix
+++ b/pkgs/development/coq-modules/gaia-hydras/default.nix
@@ -1,7 +1,7 @@
 { lib, mkCoqDerivation, coq, hydra-battles, gaia,
   mathcomp-zify, mathcomp, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "gaia-hydras";
   repo = "hydra-battles";
 
@@ -10,7 +10,7 @@ with lib; mkCoqDerivation rec {
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = with versions; switch [coq.coq-version mathcomp.version] [
+  defaultVersion = with lib.versions; lib.switch [coq.coq-version mathcomp.version] [
     { cases = [ (range "8.14" "8.16") (isGe "1.12.0") ]; out = "0.6"; }
     { cases = [ (range "8.13" "8.14") (isGe "1.12.0") ]; out = "0.5"; }
   ] null;
@@ -23,7 +23,7 @@ with lib; mkCoqDerivation rec {
 
   useDune = true;
 
-  meta = {
+  meta = with lib; {
     description = "Comparison between ordinals in Gaia and Hydra battles";
     longDescription = ''
       The Gaia and Hydra battles projects develop different notions of ordinals.
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index d4fa4a1da30..a2994dcc9b3 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -1,6 +1,6 @@
 { lib, mkCoqDerivation, coq, mathcomp, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "gaia";
 
   release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
@@ -11,7 +11,7 @@ with lib; mkCoqDerivation {
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
     { cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.15"; }
     { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; }
   ] null;
@@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
   propagatedBuildInputs =
     [ mathcomp.ssreflect mathcomp.algebra mathcomp.fingroup ];
 
-  meta = {
+  meta = with lib; {
     description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
     maintainers = with maintainers; [ Zimmi48 ];
     license = licenses.mit;
diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix
index 52e69e90d13..5a4b4b2a4d0 100644
--- a/pkgs/development/coq-modules/gappalib/default.nix
+++ b/pkgs/development/coq-modules/gappalib/default.nix
@@ -1,12 +1,12 @@
 { which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "gappalib";
   repo = "coq";
   owner = "gappa";
   domain = "gitlab.inria.fr";
   inherit version;
-  defaultVersion = if versions.range "8.8" "8.16" coq.coq-version then "1.5.2" else null;
+  defaultVersion = if lib.versions.range "8.8" "8.16" coq.coq-version then "1.5.2" else null;
   release."1.5.2".sha256 = "sha256-A021Bhqz5r2CZBayfjIiWrCIfUlejcQAfbTmOaf6QTM=";
   release."1.5.1".sha256 = "1806bq1z6q5rq2ma7d5kfbqfyfr755hjg0dq7b2llry8fx9cxjsg";
   release."1.5.0".sha256 = "1i1c0gakffxqqqqw064cbvc243yl325hxd50jmczr6mk18igk41n";
@@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
   propagatedBuildInputs = [ flocq ];
   useMelquiondRemake.logpath = "Gappa";
 
-  meta = {
+  meta = with lib; {
     description = "Coq support library for Gappa";
     license = licenses.lgpl21;
     maintainers = [ maintainers.vbgl ];
diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/coq-modules/goedel/default.nix
index 19efb786add..1b16f8c3948 100644
--- a/pkgs/development/coq-modules/goedel/default.nix
+++ b/pkgs/development/coq-modules/goedel/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "goedel";
@@ -11,13 +10,13 @@ mkCoqDerivation {
   release."8.13.0".sha256 = "0sqqkmj6wsk4xmhrnqkhcsbsrqjzn2gnk67nqzgrmjpw5danz8y5";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.11" "8.16"; out = "8.13.0"; }
   ] null;
 
   propagatedBuildInputs = [ hydra-battles pocklington ];
 
-  meta = {
+  meta = with lib; {
     description = "The Gödel-Rosser 1st incompleteness theorem in Coq";
     maintainers = with maintainers; [ siraben ];
     license = licenses.mit;
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index c2fca0a16a7..cbd919c7aa6 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -1,8 +1,6 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
 , hierarchy-builder, version ? null }:
 
-with lib;
-
 mkCoqDerivation {
   pname = "graph-theory";
 
@@ -11,13 +9,13 @@ mkCoqDerivation {
   releaseRev = v: "v${v}";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.13" "8.16"; out = "0.9"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup hierarchy-builder ];
 
-  meta = {
+  meta = with lib; {
     description = "Library of formalized graph theory results in Coq";
     longDescription = ''
       A library of formalized graph theory results, including various
diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix
index c3a815eb5c8..fc96b2abf98 100644
--- a/pkgs/development/coq-modules/heq/default.nix
+++ b/pkgs/development/coq-modules/heq/default.nix
@@ -5,13 +5,13 @@ let fetcher = {rev, repo, owner, sha256, domain, ...}:
     url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip";
     inherit sha256;
    }; in
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "heq";
   repo = "Heq";
   owner = "gil.hur";
   domain = "sf.snu.ac.kr";
   inherit version fetcher;
-  defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null;
+  defaultVersion = if lib.versions.isLt "8.8" coq.coq-version then "0.92" else null;
   release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
 
   mlPlugin = true;
@@ -22,6 +22,6 @@ with lib; mkCoqDerivation {
   meta = {
     homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/";
     description = "Heq : a Coq library for Heterogeneous Equality";
-    maintainers = with maintainers; [ jwiegley ];
+    maintainers = with lib.maintainers; [ jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
index 4f319587de9..9bcc07387b1 100644
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
 
-with lib; let hb = mkCoqDerivation {
+let hb = mkCoqDerivation {
   pname = "hierarchy-builder";
   owner = "math-comp";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.15" "8.16"; out = "1.4.0"; }
     { case = range "8.13" "8.14"; out = "1.2.0"; }
     { case = range "8.12" "8.13"; out = "1.1.0"; }
@@ -25,16 +25,16 @@ with lib; let hb = mkCoqDerivation {
 
   extraInstallFlags = [ "VFILES=structures.v" ];
 
-  meta = {
+  meta = with lib; {
     description = "High level commands to declare a hierarchy based on packed classes";
     maintainers = with maintainers; [ cohencyril siraben ];
     license = licenses.mit;
   };
 }; in
 hb.overrideAttrs (o:
-  optionalAttrs (versions.isGe "1.2.0" o.version || o.version == "dev")
+  lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev")
     { buildPhase = "make build"; }
   //
-  optionalAttrs (versions.isGe "1.1.0" o.version || o.version == "dev")
+  lib.optionalAttrs (lib.versions.isGe "1.1.0" o.version || o.version == "dev")
   { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
 )
diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix
index 2729f7c2139..06798c5fcc2 100644
--- a/pkgs/development/coq-modules/hydra-battles/default.nix
+++ b/pkgs/development/coq-modules/hydra-battles/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, equations, LibHyps, version ? null }:
-with lib;
 
 (mkCoqDerivation {
   pname = "hydra-battles";
@@ -11,14 +10,14 @@ with lib;
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.13" "8.16"; out = "0.6"; }
     { case = range "8.11" "8.12"; out = "0.4"; }
   ] null;
 
   useDune = true;
 
-  meta = {
+  meta = with lib; {
     description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
     longDescription = ''
       An exploration of some properties of Kirby and Paris' hydra
@@ -33,5 +32,5 @@ with lib;
   };
 }).overrideAttrs(o:
   let inherit (o) version; in {
-    propagatedBuildInputs = [ equations ] ++ optional (versions.isGe "0.6" version || version == "dev") LibHyps;
+    propagatedBuildInputs = [ equations ] ++ lib.optional (lib.versions.isGe "0.6" version || version == "dev") LibHyps;
   })
diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix
index a2a59e1ab22..f72dd69f361 100644
--- a/pkgs/development/coq-modules/iris/default.nix
+++ b/pkgs/development/coq-modules/iris/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, stdpp, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "iris";
   domain = "gitlab.mpi-sws.org";
   owner = "iris";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.13" "8.16"; out = "4.0.0"; }
     { case = range "8.12" "8.14"; out = "3.5.0"; }
     { case = range "8.11" "8.13"; out = "3.4.0"; }
@@ -26,7 +26,7 @@ with lib; mkCoqDerivation rec {
     fi
   '';
 
-  meta = {
+  meta = with lib; {
     description = "The Coq development of the Iris Project";
     license = licenses.bsd3;
     maintainers = [ maintainers.vbgl ];
diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix
index 1ffa37ec6c3..e2dfe98cf98 100644
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, version ? null }:
-with lib;
 
 mkCoqDerivation rec {
   pname = "itauto";
@@ -11,7 +10,7 @@ mkCoqDerivation rec {
   release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
   release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = isEq "8.16"; out = "8.16.0"; }
     { case = isEq "8.15"; out = "8.15.0"; }
     { case = isEq "8.14"; out = "8.14.0"; }
@@ -22,7 +21,7 @@ mkCoqDerivation rec {
   nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
   enableParallelBuilding = false;
 
-  meta = {
+  meta =  with lib; {
     description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
     maintainers = with maintainers; [ siraben ];
     license = licenses.gpl3Plus;
diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/coq-modules/ltac2/default.nix
index c938a7ad027..da281842960 100644
--- a/pkgs/development/coq-modules/ltac2/default.nix
+++ b/pkgs/development/coq-modules/ltac2/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, which, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "ltac2";
   owner = "coq";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = "8.10"; out = "0.3"; }
     { case = "8.9";  out = "0.2"; }
     { case = "8.8";  out = "0.1"; }
@@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     description = "A robust and expressive tactic language for Coq";
     maintainers = [ maintainers.vbgl ];
     license = licenses.lgpl21;
diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix
index da708f87e47..d40dacd3938 100644
--- a/pkgs/development/coq-modules/math-classes/default.nix
+++ b/pkgs/development/coq-modules/math-classes/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, bignums, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   pname = "math-classes";
   inherit version;
-  defaultVersion = if versions.range "8.6" "8.16" coq.coq-version then "8.15.0" else null;
+  defaultVersion = if lib.versions.range "8.6" "8.16" coq.coq-version then "8.15.0" else null;
   release."8.12.0".sha256 = "14nd6a08zncrl5yg2gzk0xf4iinwq4hxnsgm4fyv07ydbkxfb425";
   release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
   release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
@@ -14,6 +14,6 @@ with lib; mkCoqDerivation {
   meta = {
     homepage = "https://math-classes.github.io";
     description = "A library of abstract interfaces for mathematical structures in Coq.";
-    maintainers = with maintainers; [ siddharthist jwiegley ];
+    maintainers = with lib.maintainers; [ siddharthist jwiegley ];
   };
 }
diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix
index 43228252b55..bae9266d4de 100644
--- a/pkgs/development/coq-modules/mathcomp-abel/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix
@@ -7,7 +7,7 @@ mkCoqDerivation {
   owner = "math-comp";
 
   inherit version;
-  defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ]  [
+  defaultVersion = with lib; with versions; lib.switch [ coq.version mathcomp.version ]  [
       { cases = [ (range "8.10" "8.16") (range "1.12.0" "1.15.0") ]; out = "1.2.1"; }
       { cases = [ (range "8.10" "8.15") (range "1.12.0" "1.14.0") ]; out = "1.2.0"; }
       { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
index f4ae2afd386..af37096a4fb 100644
--- a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
@@ -1,14 +1,14 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra,
   coq-elpi, mathcomp-zify, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   namePrefix = [ "coq" "mathcomp" ];
   pname = "algebra-tactics";
   owner = "math-comp";
   inherit version;
 
-  defaultVersion = with versions;
-     switch [ coq.coq-version mathcomp-algebra.version ] [
+  defaultVersion = with lib.versions;
+     lib.switch [ coq.coq-version mathcomp-algebra.version ] [
        { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.0.0"; }
      ] null;
 
@@ -18,6 +18,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "Ring and field tactics for Mathematical Components";
-    maintainers = with maintainers; [ cohencyril ];
+    maintainers = with lib.maintainers; [ cohencyril ];
   };
 }
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index a42b551d184..3e67675b5ef 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -21,7 +21,7 @@ let
   release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
   release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
 
-  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+  defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ]  [
       { cases = [ (isGe "8.14") (isGe "1.13.0") ];               out = "0.5.3"; }
       { cases = [ (isGe "8.14") (range "1.13" "1.15") ];         out = "0.5.2"; }
       { cases = [ (isGe "8.13") (range "1.13" "1.14") ];         out = "0.5.1"; }
@@ -40,7 +40,7 @@ let
       classical-deps = [ mathcomp.algebra mathcomp-finmap hierarchy-builder ];
       analysis-deps = [ mathcomp.field mathcomp-bigenough ];
       intra-deps = if package == "single" then []
-        else map mathcomp_ (head (splitList (pred.equal package) packages));
+        else map mathcomp_ (head (splitList (lib.pred.equal package) packages));
       pkgpath = if package == "single" then "."
         else if package == "analysis" then "theories" else "${package}";
       pname = if package == "single" then "mathcomp-analysis-single"
diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
index 7804a61c930..a4e4a1ecbb5 100644
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
@@ -1,6 +1,6 @@
 { coq, mkCoqDerivation, mathcomp, lib, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
   pname = "bigenough";
@@ -11,7 +11,7 @@ with lib; mkCoqDerivation {
     "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
   };
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     { case = range "8.10" "8.16"; out = "1.0.1"; }
     { case = range "8.5"  "8.14"; out = "1.0.0"; }
   ] null;
@@ -20,6 +20,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "A small library to do epsilon - N reasonning";
-    license = licenses.cecill-b;
+    license = lib.licenses.cecill-b;
   };
 }
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index 8c29208c3f6..551d33c9fad 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -1,12 +1,12 @@
 { coq, mkCoqDerivation, mathcomp, lib, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
   pname = "finmap";
   owner = "math-comp";
   inherit version;
-  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
       { cases = [ (range "8.13" "8.16")  (isGe "1.12") ];         out = "1.5.2"; }
       { cases = [ (isGe "8.10")          (isGe "1.11") ];         out = "1.5.1"; }
       { cases = [ (range "8.7" "8.11")   "1.11.0" ];              out = "1.5.0"; }
@@ -33,6 +33,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "A finset and finmap library";
-    license = licenses.cecill-b;
+    license = lib.licenses.cecill-b;
   };
 }
diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
index aef912c6151..b114a3f290d 100644
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@@ -1,7 +1,7 @@
 { coq, mkCoqDerivation, mathcomp, mathcomp-bigenough,
   lib, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
   pname = "real-closed";
@@ -17,7 +17,7 @@ with lib; mkCoqDerivation {
     "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
   };
 
-  defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
       { cases = [ (isGe "8.13")  (isGe "1.12.0") ]; out = "1.1.3"; }
       { cases = [ (isGe "8.10")  (isGe "1.12.0") ]; out = "1.1.2"; }
       { cases = [ (isGe "8.7")   "1.11.0" ]; out = "1.1.1"; }
@@ -37,6 +37,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "Mathematical Components Library on real closed fields";
-    license = licenses.cecill-c;
+    license = lib.licenses.cecill-c;
   };
 }
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
index 706ee068692..19ecfcc384d 100644
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -1,14 +1,15 @@
 { coq, mkCoqDerivation, mathcomp-ssreflect, mathcomp-fingroup,
   lib, version ? null }@args:
-with lib; mkCoqDerivation {
+
+mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
   pname = "tarjan";
   owner = "math-comp";
 
   inherit version;
-  defaultVersion = with versions;
-    switch [ coq.version mathcomp-ssreflect.version ] [{
+  defaultVersion = with lib.versions;
+    lib.switch [ coq.version mathcomp-ssreflect.version ] [{
       cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.0.0";
   }] null;
   release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1";
@@ -17,6 +18,6 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "Proofs of Tarjan and Kosaraju connected components algorithms";
-    license = licenses.cecill-b;
+    license = lib.licenses.cecill-b;
   };
 }
diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix
index 5f34434b50f..090cc4567c3 100644
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-word/default.nix
@@ -1,6 +1,5 @@
 { coq, mkCoqDerivation, mathcomp, lib, version ? null }:
 
-with lib;
 mkCoqDerivation {
   namePrefix = [ "coq" "mathcomp" ];
   pname = "word";
@@ -15,13 +14,13 @@ mkCoqDerivation {
   release."1.0".sha256 = "sha256:0703m97rnivcbc7vvbd9rl2dxs6l8n52cbykynw61c6w9rhxspcg";
 
   inherit version;
-  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
     { cases = [ (range "8.12" "8.16") (isGe "1.12") ]; out = "2.0"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
 
-  meta = {
+  meta = with lib; {
     description = "Yet Another Coq Library on Machine Words";
     maintainers = [ maintainers.vbgl ];
     license = licenses.mit;
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index 1ac1d928738..86dd239ebf7 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -1,14 +1,14 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-ssreflect,  mathcomp-fingroup, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   namePrefix = [ "coq" "mathcomp" ];
   pname = "zify";
   repo = "mczify";
   owner = "math-comp";
   inherit version;
 
-  defaultVersion = with versions;
-     switch [ coq.coq-version mathcomp-algebra.version ] [
+  defaultVersion = with lib.versions;
+     lib.switch [ coq.coq-version mathcomp-algebra.version ] [
        { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; }
      ] null;
 
@@ -19,6 +19,6 @@ with lib; mkCoqDerivation rec {
 
   meta = {
     description = "Micromega tactics for Mathematical Components";
-    maintainers = with maintainers; [ cohencyril ];
+    maintainers = with lib.maintainers; [ cohencyril ];
   };
 }
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 7be30844eb0..031536b7a6e 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -18,7 +18,7 @@ let
   repo  = "math-comp";
   owner = "math-comp";
   withDoc = single && (args.withDoc or false);
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with versions; lib.switch coq.coq-version [
       { case = range "8.14" "8.16"; out = "1.15.0"; }
       { case = range "8.11" "8.15"; out = "1.14.0"; }
       { case = range "8.11" "8.15"; out = "1.13.0"; }
@@ -50,7 +50,7 @@ let
 
   mathcomp_ = package: let
       mathcomp-deps = if package == "single" then []
-        else map mathcomp_ (head (splitList (pred.equal package) packages));
+        else map mathcomp_ (head (splitList (lib.pred.equal package) packages));
       pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
       pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
       pkgallMake = ''
diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix
index ab036add60b..9a22d82dd40 100644
--- a/pkgs/development/coq-modules/metacoq/default.nix
+++ b/pkgs/development/coq-modules/metacoq/default.nix
@@ -5,7 +5,7 @@ with builtins // lib;
 let
   repo  = "metacoq";
   owner = "MetaCoq";
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with versions; lib.switch coq.coq-version [
       { case = "8.11"; out = "1.0-beta2-8.11"; }
       { case = "8.12"; out = "1.0-beta2-8.12"; }
       # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
@@ -34,7 +34,7 @@ let
 
   metacoq_ = package: let
       metacoq-deps = if package == "single" then []
-        else map metacoq_ (head (splitList (pred.equal package) packages));
+        else map metacoq_ (head (splitList (lib.pred.equal package) packages));
       pkgpath = if package == "single" then "./" else "./${package}";
       pname = if package == "all" then "metacoq" else "metacoq-${package}";
       pkgallMake = ''
diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix
index 6072f9995c0..82d2a16f77f 100644
--- a/pkgs/development/coq-modules/metalib/default.nix
+++ b/pkgs/development/coq-modules/metalib/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "metalib";
   owner = "plclub";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.14" "8.16"; out = "8.15"; }
     { case = range "8.10" "8.13"; out = "8.10"; }
   ] null;
@@ -14,7 +14,7 @@ with lib; mkCoqDerivation {
 
   sourceRoot = "source/Metalib";
 
-  meta = {
+  meta = with lib; {
     license = licenses.mit;
     maintainers = [ maintainers.jwiegley ];
   };
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 57f4a381b20..19c6015ce92 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -1,6 +1,6 @@
 { coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
   lib, version ? null, useDune ? false }@args:
-with lib; mkCoqDerivation {
+ mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
   pname = "multinomials";
@@ -8,7 +8,7 @@ with lib; mkCoqDerivation {
   owner = "math-comp";
 
   inherit version;
-  defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
+  defaultVersion =  with lib.versions; lib.switch [ coq.version mathcomp.version ] [
       { cases = [ (isGe "8.10") (isGe "1.12.0") ];      out = "1.5.5"; }
       { cases = [ (range "8.10" "8.12") "1.12.0" ];             out = "1.5.3"; }
       { cases = [ (range "8.7" "8.12")  "1.11.0" ];             out = "1.5.2"; }
@@ -31,7 +31,7 @@ with lib; mkCoqDerivation {
     "1.0".sha256   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
   };
 
-  useDuneifVersion = v: versions.isGe "1.5.3" v || v == "dev";
+  useDuneifVersion = v: lib.versions.isGe "1.5.3" v || v == "dev";
 
   preConfigure = ''
     patchShebangs configure || true
@@ -42,7 +42,7 @@ with lib; mkCoqDerivation {
 
   meta = {
     description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
-    license = licenses.cecill-c;
+    license = lib.licenses.cecill-c;
   };
 }
-// optionalAttrs (args?useDune) { inherit useDune; }
+// lib.optionalAttrs (args?useDune) { inherit useDune; }
diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
index 066976e8b4b..b6770aa633d 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, mathcomp, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "odd-order";
@@ -11,7 +10,7 @@ mkCoqDerivation {
   releaseRev = v: "mathcomp-odd-order.${v}";
 
   inherit version;
-  defaultVersion = with versions; switch mathcomp.character.version [
+  defaultVersion = with lib.versions; lib.switch mathcomp.character.version [
     { case = (range "1.13.0" "1.15.0"); out = "1.14.0"; }
     { case = (range "1.12.0" "1.14.0"); out = "1.13.0"; }
     { case = (range "1.10.0" "1.12.0"); out = "1.12.0"; }
@@ -27,7 +26,7 @@ mkCoqDerivation {
     mathcomp.all
   ];
 
-  meta = {
+  meta = with lib; {
     description = "Formal proof of the Odd Order Theorem";
     maintainers = with maintainers; [ siraben ];
     license = licenses.cecill-b;
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
index ea0988ef607..e9163c16132 100644
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@@ -1,10 +1,10 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "paco";
   owner = "snu-sf";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.12" "8.16"; out = "4.1.2"; }
     { case = range "8.9" "8.13"; out = "4.1.1"; }
     { case = range "8.6" "8.13"; out = "4.0.2"; }
@@ -27,6 +27,6 @@ with lib; mkCoqDerivation {
   meta = {
     homepage = "https://plv.mpi-sws.org/paco/";
     description = "A Coq library implementing parameterized coinduction";
-    maintainers = with maintainers; [ jwiegley ptival ];
+    maintainers = with lib.maintainers; [ jwiegley ptival ];
   };
 }
diff --git a/pkgs/development/coq-modules/paramcoq/default.nix b/pkgs/development/coq-modules/paramcoq/default.nix
index e03f44320cf..cc4966affcf 100644
--- a/pkgs/development/coq-modules/paramcoq/default.nix
+++ b/pkgs/development/coq-modules/paramcoq/default.nix
@@ -1,9 +1,9 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "paramcoq";
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     { case = range "8.10" "8.16"; out = "1.1.3+coq${coq.coq-version}"; }
     { case = range "8.7"  "8.13"; out = "1.1.2+coq${coq.coq-version}"; }
   ] null;
@@ -24,7 +24,7 @@ with lib; mkCoqDerivation {
   release."1.1.2+coq8.7".sha256  = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj";
   releaseRev = v: "v${v}";
   mlPlugin = true;
-  meta = {
+  meta = with lib; {
     description = "Coq plugin for parametricity";
     license = licenses.mit;
     maintainers = [ maintainers.vbgl ];
diff --git a/pkgs/development/coq-modules/parsec/default.nix b/pkgs/development/coq-modules/parsec/default.nix
index f764267d77e..8a30fbeb961 100644
--- a/pkgs/development/coq-modules/parsec/default.nix
+++ b/pkgs/development/coq-modules/parsec/default.nix
@@ -1,6 +1,5 @@
 { lib, mkCoqDerivation, coq, ceres, coq-ext-lib, version ? null }:
 
-with lib;
 mkCoqDerivation {
 
   pname = "parsec";
@@ -11,14 +10,14 @@ mkCoqDerivation {
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     { case = range "8.12" "8.16"; out = "0.1.1"; }
     { case = range "8.12" "8.13"; out = "0.1.0"; }
   ] null;
   release."0.1.1".sha256 = "sha256:1c0l18s68pzd4c8i3jimh2yz0pqm4g38pca4bm7fr18r8xmqf189";
   release."0.1.0".sha256 = "sha256:01avfcqirz2b9wjzi9iywbhz9szybpnnj3672dgkfsimyg9jgnsr";
 
-  meta = {
+  meta = with lib; {
     description = "Library for serialization to S-expressions";
     license = licenses.bsd3;
     maintainers = with maintainers; [ Zimmi48 ];
diff --git a/pkgs/development/coq-modules/pocklington/default.nix b/pkgs/development/coq-modules/pocklington/default.nix
index 111bffeca2c..a9e0d43a5a7 100644
--- a/pkgs/development/coq-modules/pocklington/default.nix
+++ b/pkgs/development/coq-modules/pocklington/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "pocklington";
@@ -9,11 +8,11 @@ mkCoqDerivation {
   release."8.12.0".sha256 = "sha256-0xBrw9+4g14niYdNqp0nx00fPJoSSnaDSDEaIVpPfjs=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = isGe "8.7"; out = "8.12.0"; }
   ] null;
 
-  meta = {
+  meta = with lib; {
     description = "Pocklington's criterion for primality in Coq";
     maintainers = with maintainers; [ siraben ];
     license = licenses.mit;
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix
index 2d83cbfd883..44e938e16db 100644
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, ssreflect, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "reglang";
@@ -9,14 +8,14 @@ mkCoqDerivation {
   release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "1.1.2"; }
   ] null;
 
 
   propagatedBuildInputs = [ ssreflect ];
 
-  meta = {
+  meta = with lib; {
     description = "Regular Language Representations in Coq";
     maintainers = with maintainers; [ siraben ];
     license = licenses.cecill-b;
diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix
index d2124d56f3f..c8fb6982b84 100644
--- a/pkgs/development/coq-modules/relation-algebra/default.nix
+++ b/pkgs/development/coq-modules/relation-algebra/default.nix
@@ -1,12 +1,11 @@
 { lib, mkCoqDerivation, coq, aac-tactics, mathcomp, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "relation-algebra";
   owner = "damien-pous";
 
   releaseRev = v:
-    if versions.isGe "1.7.6" v
+    if lib.versions.isGe "1.7.6" v
     then "v.${v}"
     else "v${v}";
 
@@ -20,7 +19,7 @@ mkCoqDerivation {
   release."1.7.1".sha256 = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = isEq "8.16"; out = "1.7.8"; }
     { case = isEq "8.15"; out = "1.7.7"; }
     { case = isEq "8.14"; out = "1.7.6"; }
@@ -35,7 +34,7 @@ mkCoqDerivation {
 
   propagatedBuildInputs = [ aac-tactics mathcomp.ssreflect ];
 
-  meta = {
+  meta = with lib; {
     description = "Relation algebra library for Coq";
     maintainers = with maintainers; [ siraben ];
     license = licenses.gpl3Plus;
diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix
index ecbef5b92fe..468be219d0d 100644
--- a/pkgs/development/coq-modules/semantics/default.nix
+++ b/pkgs/development/coq-modules/semantics/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, version ? null }:
-with lib;
 
 mkCoqDerivation rec {
   pname = "semantics";
@@ -15,7 +14,7 @@ mkCoqDerivation rec {
   release."8.6.0".sha256 = "sha256-GltkGQ3tJqUPAbdDkqqvKLLhMOap50XvGaCkjshiNdY=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "8.14.0"; }
     { case = "8.9"; out = "8.9.0"; }
     { case = "8.8"; out = "8.8.0"; }
@@ -34,7 +33,7 @@ mkCoqDerivation rec {
     done
   '';
 
-  meta = {
+  meta = with lib; {
     description = "A survey of programming language semantics styles in Coq";
     longDescription = ''
       A survey of semantics styles in Coq, from natural semantics through
diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix
index e3ec9bfdc39..27641f4f5a9 100644
--- a/pkgs/development/coq-modules/serapi/default.nix
+++ b/pkgs/development/coq-modules/serapi/default.nix
@@ -17,7 +17,7 @@ in
   inherit version release;
 
   defaultVersion =  with versions;
-    switch coq.version [
+    lib.switch coq.version [
       { case = isEq "8.16"; out = "8.16.0+0.16.0"; }
       { case = isEq "8.15"; out = "8.15.0+0.15.0"; }
       { case = isEq "8.14"; out = "8.14.0+0.14.0"; }
diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix
index f9fe909d8ca..509ce57c5cf 100644
--- a/pkgs/development/coq-modules/simple-io/default.nix
+++ b/pkgs/development/coq-modules/simple-io/default.nix
@@ -1,11 +1,11 @@
 { lib, callPackage, mkCoqDerivation, coq, coq-ext-lib, version ? null }:
 
-with lib; mkCoqDerivation {
+mkCoqDerivation {
   pname = "simple-io";
   owner = "Lysxia";
   repo = "coq-simple-io";
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.11" "8.16"; out = "1.7.0"; }
     { case = range "8.7"  "8.13"; out = "1.3.0"; }
   ] null;
@@ -21,7 +21,7 @@ with lib; mkCoqDerivation {
 
   passthru.tests.HelloWorld = callPackage ./test.nix {};
 
-  meta = {
+  meta = with lib; {
     description = "Purely functional IO for Coq";
     license = licenses.mit;
     maintainers = [ maintainers.vbgl ];
diff --git a/pkgs/development/coq-modules/smpl/default.nix b/pkgs/development/coq-modules/smpl/default.nix
index f03065cf045..2ba755dd42d 100644
--- a/pkgs/development/coq-modules/smpl/default.nix
+++ b/pkgs/development/coq-modules/smpl/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "smpl";
@@ -13,7 +12,7 @@ mkCoqDerivation {
   releaseRev = v: "v${v}";
 
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     { case = isEq "8.15"; out = "8.15"; }
     { case = isEq "8.14"; out = "8.14"; }
     { case = "8.13.2"; out = "8.13"; }
@@ -23,7 +22,7 @@ mkCoqDerivation {
 
   mlPlugin = true;
 
-  meta = {
+  meta = with lib; {
     description = "A Coq plugin providing an extensible tactic similar to first";
     maintainers = with maintainers; [ siraben ];
     license = licenses.mit;
diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/coq-modules/smtcoq/default.nix
index 89a6abd2b1a..49c4348b9af 100644
--- a/pkgs/development/coq-modules/smtcoq/default.nix
+++ b/pkgs/development/coq-modules/smtcoq/default.nix
@@ -1,5 +1,4 @@
 { lib, stdenv, gcc10StdenvCompat, pkgs, mkCoqDerivation, coq, trakt, veriT, zchaff, fetchurl, version ? null }:
-with lib;
 
 let
   # version of veriT that works with SMTCoq
@@ -23,7 +22,7 @@ mkCoqDerivation {
   release."2021-09-17".sha256 = "sha256-bF7ES+tXraaAJwVEwAMx3CUESpNlAUerQjr4d2eaGJQ=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.version [
+  defaultVersion = with lib.versions; lib.switch coq.version [
     { case = isEq "8.13"; out = "2021-09-17"; }
   ] null;
 
@@ -34,7 +33,7 @@ mkCoqDerivation {
   # This is meant to ease future troubleshooting of cvc4 build failures
   passthru = { inherit cvc4; };
 
-  meta = {
+  meta = with lib; {
     description = "Communication between Coq and SAT/SMT solvers ";
     maintainers = with maintainers; [ siraben ];
     license = licenses.cecill-b;
diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix
index 19b72c4e948..d20b6373214 100644
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ b/pkgs/development/coq-modules/stdpp/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; mkCoqDerivation rec {
+mkCoqDerivation rec {
   pname = "stdpp";
   inherit version;
   domain = "gitlab.mpi-sws.org";
   owner = "iris";
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.13" "8.16"; out = "1.8.0"; }
     { case = range "8.12" "8.14"; out = "1.6.0"; }
     { case = range "8.11" "8.13"; out = "1.5.0"; }
@@ -24,7 +24,7 @@ with lib; mkCoqDerivation rec {
     fi
   '';
 
-  meta = {
+  meta = with lib; {
     description = "An extended “Standard Library” for Coq";
     license = licenses.bsd3;
     maintainers = [ maintainers.vbgl ];
diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/coq-modules/tlc/default.nix
index 79d3ce2d7a0..8ded1abeb14 100644
--- a/pkgs/development/coq-modules/tlc/default.nix
+++ b/pkgs/development/coq-modules/tlc/default.nix
@@ -1,11 +1,11 @@
 { lib, mkCoqDerivation, coq, version ? null }:
 
-with lib; (mkCoqDerivation {
+(mkCoqDerivation {
   pname = "tlc";
   owner = "charguer";
   inherit version;
   displayVersion = { tlc = false; };
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.13" "8.16"; out = "20211215"; }
     { case = range "8.12" "8.13"; out = "20210316"; }
     { case = range "8.10" "8.12"; out = "20200328"; }
@@ -16,14 +16,14 @@ with lib; (mkCoqDerivation {
   release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx";
   release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl";
 
-  meta = {
+  meta = with lib; {
     homepage = "http://www.chargueraud.org/softs/tlc/";
     description = "A non-constructive library for Coq";
     license = licenses.free;
     maintainers = [ maintainers.vbgl ];
   };
 }).overrideAttrs (x:
-  if versionAtLeast x.version "20210316"
+  if lib.versionAtLeast x.version "20210316"
   then {}
   else {
     installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ];
diff --git a/pkgs/development/coq-modules/topology/default.nix b/pkgs/development/coq-modules/topology/default.nix
index 71849c50ae9..de73fbadbf0 100644
--- a/pkgs/development/coq-modules/topology/default.nix
+++ b/pkgs/development/coq-modules/topology/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, mathcomp, zorns-lemma, version ? null }:
-with lib;
 
 mkCoqDerivation rec {
   pname = "topology";
@@ -15,7 +14,7 @@ mkCoqDerivation rec {
   release."8.6.0".sha256 = "sha256-eu/dBEFo3y6vnXlJljUD4hds6+qgAPQVvsuspyGHcj8=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "9.0.0"; }
     { case = "8.9"; out = "8.9.0"; }
     { case = "8.8"; out = "8.8.0"; }
@@ -25,9 +24,9 @@ mkCoqDerivation rec {
 
   propagatedBuildInputs = [ zorns-lemma ];
 
-  useDuneifVersion = versions.isGe "9.0";
+  useDuneifVersion = lib.versions.isGe "9.0";
 
-  meta = {
+  meta = with lib; {
     description = "General topology in Coq";
     longDescription = ''
       This library develops some of the basic concepts and results of
diff --git a/pkgs/development/coq-modules/trakt/default.nix b/pkgs/development/coq-modules/trakt/default.nix
index f10e69cc4e9..8bc7581489c 100644
--- a/pkgs/development/coq-modules/trakt/default.nix
+++ b/pkgs/development/coq-modules/trakt/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
-with lib;
 
 mkCoqDerivation {
   pname = "trakt";
@@ -9,13 +8,13 @@ mkCoqDerivation {
   release."1.0".sha256 = "sha256-Qhw5fWFYxUFO2kIWWz/og+4fuy9aYG27szfNk3IglhY=";
 
   inherit version;
-  defaultVersion = with versions; switch [ coq.version ] [
+  defaultVersion = with lib.versions; lib.switch [ coq.version ] [
     { cases = [ (range "8.13" "8.16") ]; out = "1.0"; }
   ] null;
 
   propagatedBuildInputs = [ coq-elpi ];
 
-  meta = {
+  meta = with lib; {
     description = "A generic goal preprocessing tool for proof automation tactics in Coq";
     maintainers = with maintainers; [ siraben ];
     license = licenses.cecill-b;
diff --git a/pkgs/development/coq-modules/zorns-lemma/default.nix b/pkgs/development/coq-modules/zorns-lemma/default.nix
index dedb58b5935..19696bd81d4 100644
--- a/pkgs/development/coq-modules/zorns-lemma/default.nix
+++ b/pkgs/development/coq-modules/zorns-lemma/default.nix
@@ -1,5 +1,4 @@
 { lib, mkCoqDerivation, coq, version ? null }:
-with lib;
 
 (mkCoqDerivation {
   pname = "zorns-lemma";
@@ -16,7 +15,7 @@ with lib;
   release."8.5.0".sha256 = "sha256-mH/v02ObMjbVPYx2H+Jhz+Xp0XRKN67iMAdA1VNFzso=";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
+  defaultVersion = with lib.versions; lib.switch coq.coq-version [
     { case = range "8.10" "8.16"; out = "9.0.0"; }
     { case = "8.9"; out = "8.9.0"; }
     { case = "8.8"; out = "8.8.0"; }
@@ -25,9 +24,9 @@ with lib;
     { case = "8.5"; out = "8.5.0"; }
   ] null;
 
-  useDuneifVersion = versions.isGe "9.0";
+  useDuneifVersion = lib.versions.isGe "9.0";
 
-  meta = {
+  meta = with lib; {
     description = "Development of basic set theory";
     longDescription = ''
       This Coq library develops some basic set theory.  The main
@@ -37,4 +36,4 @@ with lib;
     maintainers = with maintainers; [ siraben ];
     license = licenses.lgpl21Plus;
   };
-}).overrideAttrs({version, ...}: if versions.isGe "9.0" version then { repo =  "topology"; } else {})
+}).overrideAttrs({version, ...}: if lib.versions.isGe "9.0" version then { repo =  "topology"; } else {})