diff --git a/lib/default.nix b/lib/default.nix
index ccae0bbc3ab41..3526f671e62c9 100644
--- a/lib/default.nix
+++ b/lib/default.nix
@@ -15,11 +15,15 @@ let
     trivial = callLibs ./trivial.nix;
     fixedPoints = callLibs ./fixed-points.nix;
 
+    # control flow
+    switchs = callLibs ./switchs.nix;
+
     # datatypes
     attrsets = callLibs ./attrsets.nix;
     lists = callLibs ./lists.nix;
     strings = callLibs ./strings.nix;
     stringsWithDeps = callLibs ./strings-with-deps.nix;
+    preds = callLibs ./preds.nix;
 
     # packaging
     customisation = callLibs ./customisation.nix;
@@ -71,6 +75,7 @@ let
       toHexString toBaseDigits;
     inherit (self.fixedPoints) fix fix' converge extends composeExtensions
       composeManyExtensions makeExtensible makeExtensibleWithCustomName;
+    inherit (self.switchs) switch-if switch;
     inherit (self.attrsets) attrByPath hasAttrByPath setAttrByPath
       getAttrFromPath attrVals attrValues getAttrs catAttrs filterAttrs
       filterAttrsRecursive foldAttrs collect nameValuePair mapAttrs
@@ -81,7 +86,7 @@ let
       getLib getDev getMan chooseDevOutputs zipWithNames zip
       recurseIntoAttrs dontRecurseIntoAttrs cartesianProductOfSets;
     inherit (self.lists) singleton forEach foldr fold foldl foldl' imap0 imap1
-      concatMap flatten remove findSingle findFirst any all count
+      concatMap flatten remove findSingle findFirst splitList any all count
       optional optionals toList range partition zipListsWith zipLists
       reverseList listDfs toposort sort naturalSort compareLists take
       drop sublist last init crossLists unique intersectLists
diff --git a/lib/lists.nix b/lib/lists.nix
index e469f3ef26526..b411b49ee0d1e 100644
--- a/lib/lists.nix
+++ b/lib/lists.nix
@@ -200,6 +200,46 @@ rec {
     let found = filter pred list;
     in if found == [] then default else head found;
 
+  /* Takes a predicate and a list as input and
+     returns a list of lists, separated by elements that match the predicate.
+
+     This is analoguous to `builtins.split separator string`,
+     with a predicate instead of a separator
+     and a list instead of a string.
+
+     Type: splitList :: (a -> bool) -> [a] -> [ (a | [a]) ]
+
+     The returned list always has the form `[ [...] sep [...] ... sep [...] ]`
+     i.e. begins with a list, alternates with separators and ends with a list,
+     so that the following is true for `res = splitList pred l`:
+     - `res` has length `2 * k + 1`,
+       where `k` is the number of elements of `l` that
+       match `pred`. (ie `splitList pred l`)
+     - `elemAt res (2 * n)` is always a list,
+       which contains no element matching `pred`.
+     - `elemAt res (2 * n + 1)` is always a single element that matches `pred`.
+
+     Ie, for all `pred` and `l`, let `k = length (filter pred l)`, we have:
+     - `length (splitList pred l) = 2 * k + 1`,
+     - `isList (elemAt (splitList pred l) (2 * n))`, for all `n <= k`,
+     - `pred (elemAt (splitList pred l) (2 * n + 1))`, for all `n < k`,
+     - `flatten (map (pick (splitList pred l)) (range 0 (2 * k))) == l`, where
+       `pick = r: n: (if mod n 2 == 1 then singleton else id) (elemAt r n)`
+
+     Examples:
+     - splitList (x: x == "x") [ "y" "x" "z" "t" ]
+       => [ [ "y" ] "x" [ "z" "t" ] ]
+     - splitList (x: false) l == [ l ]
+     - splitList (x: x < 2) [ 2 1 3 4 0 1 3 1 ]
+       => [ [ 2 ] 1 [ 3 4 ] 0 [ ] 1 [ 3 ] 1 [ ] ]
+
+  */
+  splitList = pred: l:
+    let loop = (vv: v: l: if l == [] then vv ++ [v]
+      else let hd = head l; tl = tail l; in
+      if pred hd then loop (vv ++ [ v hd ]) [] tl else loop vv (v ++ [hd]) tl);
+    in loop [] [] l;
+
   /* Return true if function `pred` returns true for at least one
      element of `list`.
 
diff --git a/lib/preds.nix b/lib/preds.nix
new file mode 100644
index 0000000000000..b4a164afa43e2
--- /dev/null
+++ b/lib/preds.nix
@@ -0,0 +1,17 @@
+{ lib }:
+with lib; {
+  /* Constant predicates: true and false */
+  true  = p: true;
+  false = p: false;
+
+  /* Predicate intersection, union, complement,
+     difference and implication */
+  inter = p: q: x: p x && q x;
+  union = p: q: x: p x || q x;
+  compl = p:    x: ! p x;
+  diff  = p: q: preds.inter p (preds.compl q);
+  impl  = p: q: x: p x -> q x;
+
+  /* predicate "being equal to x" */
+  equal = x: y: y == x;
+}
diff --git a/lib/switchs.nix b/lib/switchs.nix
new file mode 100644
index 0000000000000..bf8643a60325b
--- /dev/null
+++ b/lib/switchs.nix
@@ -0,0 +1,75 @@
+{ lib }:
+with lib; {
+  /* Emulate a "switch - case" construct,
+   instead of relying on `if then else if ...` */
+
+  /* Usage:
+       ```nix
+       switch-if [
+         if-clause-1
+         ..
+         if-clause-k
+       ] default-out
+       ```
+       where a if-clause has the form `{ cond = b; out = r; }`
+       the first branch such as `b` is true
+
+     Example:
+       ```nix
+       let alphanum = n: switch-if [
+           { cond = n == 0; out = "zero"; }
+           { cond = n == 1; out = "one";  }
+         ] "I do not count beyond one"; in
+       [ (alphanum 0) (alphanum 1) (alphanum 42) ]
+       ```
+      => `[ "zero" "one" "I do not count beyond one" ]`
+
+  */
+  switch-if = c: d: (findFirst (getAttr "cond") {} c).out or d;
+
+  /* Usage:
+       ```nix
+       switch x [
+         simple-clause-1
+         ..
+         simple-clause-k
+       ] default-out
+       ```
+       where a simple-clause has the form `{ case = p; out = r; }`
+       the first branch such as `p x` is true
+       or
+       ```nix
+       switch [ x1 .. xn ] [
+         complex-clause-1
+         ..
+         complex-clause-k
+       ] default-out
+       ```
+       where a complex-clause is either a simple-clause
+       or has the form { cases = [ p1 .. pn ]; out = r; }
+       in which case the first branch such as all `pi xi` are true
+
+       if the variables p are not functions,
+       they are converted to a `equal p`
+       if `out` is missing then `default-out` is taken
+
+     Example:
+       ```nix
+       let test = v1: v2: with versions; switch [ v1 v2 ] [
+           { cases = [ (x: x * 2 < 4) 8 ]; out = "small, 8"; }
+           { case  = [ 42 42 ]; }          # no `out` means `default-out`
+           { case  = l: fold add 0 l > 42; out = "sum over 42"; }
+           { case  = [ 0 1 ];              out = "zero, one"; }
+         ] "weird"; in
+       [ (test 1 8) (test 40 3) (test 0 1) (test 42 42) (test 1 0)]
+       ```
+      => `[ "small, 8" "sum over 42" "zero, one" "weird" "weird" ]`
+  */
+  switch = var: clauses: default: with preds; let
+      compare = f:  if isFunction f then f else equal f;
+      combine = cl: var:
+        if cl?case then compare cl.case var
+        else all (equal true) (zipListsWith compare cl.cases var); in
+    switch-if (map (cl: { cond = combine cl var;
+                          out = cl.out or default; }) clauses) default;
+}
diff --git a/lib/versions.nix b/lib/versions.nix
index 0e9d81ac78b1e..af9e47b53ee1b 100644
--- a/lib/versions.nix
+++ b/lib/versions.nix
@@ -1,13 +1,29 @@
 /* Version string functions. */
 { lib }:
 
-rec {
+with lib;
+let
+  truncate = n: v: concatStringsSep "." (take n (splitVersion v));
+  opTruncate = op: v0: v: let n = length (splitVersion v0); in
+     op (truncate n v) (truncate n v0);
+in rec {
 
   /* Break a version string into its component parts.
 
      Example:
        splitVersion "1.2.3"
        => ["1" "2" "3"]
+
+     Remark: the builtins version of `splitVersion` -- which is
+     considered first -- has a behaviour which is different from
+     `(lib.splitString ".")`. For example, it also recognizes `-` and
+     transitions between numbers and other strings as delimiters.
+     This behaviour is hence inconsistent between versions of nix and
+     should not be relied upon.
+
+     Example (discouraged):
+       splitVersion "1-2a+3"
+       => [ "1" "2" "a+" "3" ]
   */
   splitVersion = builtins.splitVersion or (lib.splitString ".");
 
@@ -35,6 +51,17 @@ rec {
   */
   patch = v: builtins.elemAt (splitVersion v) 2;
 
+  /* Get string of the first n parts of a version string.
+
+    Example:
+    - truncate 2 "1.2.3-stuff"
+      => "1.2"
+    - truncate 4 "1.2.3-stuff"
+      => "1.2.3.stuff"
+  */
+
+  inherit truncate;
+
   /* Get string of the first two parts (major and minor)
      of a version string.
 
@@ -42,8 +69,88 @@ rec {
        majorMinor "1.2.3"
        => "1.2"
   */
-  majorMinor = v:
-    builtins.concatStringsSep "."
-    (lib.take 2 (splitVersion v));
+  majorMinor = truncate 2;
+
+  /* Get string of the first three parts (major, minor and patch)
+     of a version string.
+
+    Example:
+      majorMinorPatch "1.2.3-stuff"
+      => "1.2.3"
+  */
+  majorMinorPatch = truncate 3;
+
+  /* Version comparison predicates,
+    - isGe v0 v <-> v is greater or equal than v0   [*]
+    - isLe v0 v <-> v is lesser  or equal than v0   [*]
+    - isGt v0 v <-> v is strictly greater than v0   [*]
+    - isLt v0 v <-> v is strictly lesser  than v0   [*]
+    - isEq v0 v <-> v is equal to v0                [*]
+    - range low high v <-> v is between low and high [**]
+
+    [*]  truncating v to the same number of digits as v0
+    [**] truncating v to low for the lower bound and high for the upper bound
+
+    Difference with `versionAtLeast` and `versionOlder`:
+    - `versionAtLeast` and `versionOlder` implement order relations on
+      version numbers, which are total assuming the only separator
+      which is used is `.`.
+
+    - `isGe`, `isLe`, `isLt`, and `isEq` are not order relations, they
+    are not antisymmetric (e.g. both `isLe "1.1" "1.1.2"` and `isLe
+    "1.1.2" "1.1"` are true).
+    `(isLe x) y` reads «`y` is a version which is lesser or equal to `x`».
+    Contrarily to `versionAtLeast`, it uses the first argument to
+    determine the length to truncate so that `isLe "1.1" "1.1.2"` is
+    true while `versionAtLeast "1.1" "1.1.2"` is false.
+
+    The main motivation is to be able to combine and read them nicely
+    with high order function such as:
+    - `filter`, e.g. the result of
+      ```
+      filter (versionAtLeast "1.0")
+             [ "1.3.1" "1.0.0" "1.0" "0.9.0" "1.0.2" ]
+      ```
+      is `[ "1.0" "0.9.0"]`.
+      In comparison
+      ```
+      filter (isLe "1.0")
+             [ "1.3.1" "1.0.0" "1.0" "0.9.0" "1.0.2" ]`
+      ```
+      returns `[ "1.0.0" "1.0" "0.9.0" "1.0.2" ]`, which can be read
+      naturally in English as «we keep versions that are lesser or
+      equal to "1.0"» and the outcome matches the expectations that
+      "1.0.0" and "1.0.2" belong to the family of "1.0" versions.
+        If you wanted to filter more precisely you should give the
+      patch version of the first argument of `isLe` instead (as in
+      `isLe "1.0.0"`, and if you wanted to exclude all "1.0", then you
+      should use `isLt "1.0"`.
+    - `switch` as in:
+      pkgs/development/coq-modules/mathcomp/default.nix#L21-L22
+
+    Examples:
+    - isGe "8.10" "8.10.1"
+      => true
+    - isLe "8.10" "8.10.1"
+      => true
+    - isGt "8.10" "8.10.1"
+      => false
+    - isGt "8.10.0" "8.10.1"
+      => true
+    - isEq "8.10" "8.10.1"
+      => true
+    - range "8.10" "8.11" "8.11.1"
+      => true
+    - range "8.10" "8.11+" "8.11.0"
+      => false
+    - range "8.10" "8.11+" "8.11+beta1"
+      => false
+  */
+  isGe = opTruncate versionAtLeast;
+  isGt = opTruncate (flip versionOlder);
+  isLe = opTruncate (flip versionAtLeast);
+  isLt = opTruncate versionOlder;
+  isEq = opTruncate preds.equal;
+  range = low: high: preds.inter (versions.isGe low) (versions.isLe high);
 
 }
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 9d6212fef1126..3fba374644a1b 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -13,8 +13,6 @@
 , csdp ? null
 , version, coq-version ? null,
 }@args:
-let lib' = lib; in
-let lib = import ../../../../build-support/coq/extra-lib.nix {lib = lib';}; in
 with builtins; with lib;
 let
   release = {
diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix
index 03922303ee346..46974335e47bd 100644
--- a/pkgs/build-support/coq/default.nix
+++ b/pkgs/build-support/coq/default.nix
@@ -1,5 +1,4 @@
 { lib, stdenv, coqPackages, coq, fetchzip }@args:
-let lib = import ./extra-lib.nix {inherit (args) lib;}; in
 with builtins; with lib;
 let
   isGitHubDomain = d: match "^github.*" d != null;
@@ -74,7 +73,7 @@ stdenv.mkDerivation (removeAttrs ({
 
   meta = ({ platforms = coq.meta.platforms; } //
     (switch domain [{
-        case = pred.union isGitHubDomain isGitLabDomain;
+        case = preds.union isGitHubDomain isGitLabDomain;
         out = { homepage = "https://${domain}/${owner}/${repo}"; };
       }] {}) //
     optionalAttrs (fetched.broken or false) { coqFilter = true; broken = true; }) //
diff --git a/pkgs/build-support/coq/extra-lib.nix b/pkgs/build-support/coq/extra-lib.nix
deleted file mode 100644
index 65b48f511267f..0000000000000
--- a/pkgs/build-support/coq/extra-lib.nix
+++ /dev/null
@@ -1,145 +0,0 @@
-{ lib }:
-with builtins; with lib; recursiveUpdate lib (rec {
-
-  versions =
-    let
-      truncate = n: v: concatStringsSep "." (take n (splitVersion v));
-      opTruncate = op: v0: v: let n = length (splitVersion v0); in
-         op (truncate n v) (truncate n v0);
-    in rec {
-
-    /* Get string of the first n parts of a version string.
-
-       Example:
-       - truncate 2 "1.2.3-stuff"
-         => "1.2"
-
-       - truncate 4 "1.2.3-stuff"
-         => "1.2.3.stuff"
-    */
-
-    inherit truncate;
-
-    /* Get string of the first three parts (major, minor and patch)
-       of a version string.
-
-       Example:
-         majorMinorPatch "1.2.3-stuff"
-         => "1.2.3"
-    */
-    majorMinorPatch = truncate 3;
-
-    /* Version comparison predicates,
-      - isGe v0 v <-> v is greater or equal than v0   [*]
-      - isLe v0 v <-> v is lesser  or equal than v0   [*]
-      - isGt v0 v <-> v is strictly greater than v0   [*]
-      - isLt v0 v <-> v is strictly lesser  than v0   [*]
-      - isEq v0 v <-> v is equal to v0                [*]
-      - range low high v <-> v is between low and high [**]
-
-    [*]  truncating v to the same number of digits as v0
-    [**] truncating v to low for the lower bound and high for the upper bound
-
-      Examples:
-      - isGe "8.10" "8.10.1"
-        => true
-      - isLe "8.10" "8.10.1"
-        => true
-      - isGt "8.10" "8.10.1"
-        => false
-      - isGt "8.10.0" "8.10.1"
-        => true
-      - isEq "8.10" "8.10.1"
-        => true
-      - range "8.10" "8.11" "8.11.1"
-        => true
-      - range "8.10" "8.11+" "8.11.0"
-        => false
-      - range "8.10" "8.11+" "8.11+beta1"
-        => false
-
-    */
-    isGe = opTruncate versionAtLeast;
-    isGt = opTruncate (flip versionOlder);
-    isLe = opTruncate (flip versionAtLeast);
-    isLt = opTruncate versionOlder;
-    isEq = opTruncate pred.equal;
-    range = low: high: pred.inter (versions.isGe low) (versions.isLe high);
-  };
-
-  /* Returns a list of list, splitting it using a predicate.
-     This is analoguous to builtins.split sep list,
-     with a predicate as a separator and a list instead of a string.
-
-    Type: splitList :: (a -> bool) -> [a] -> [[a]]
-
-    Example:
-      splitList (x: x == "x") [ "y" "x" "z" "t" ]
-      => [ [ "y" ] "x" [ "z" "t" ] ]
-  */
-  splitList = pred: l: # put in file lists
-    let loop = (vv: v: l: if l == [] then vv ++ [v]
-      else let hd = head l; tl = tail l; in
-      if pred hd then loop (vv ++ [ v hd ]) [] tl else loop vv (v ++ [hd]) tl);
-    in loop [] [] l;
-
-  pred = {
-    /* Predicate intersection, union, and complement */
-    inter = p: q: x: p x && q x;
-    union = p: q: x: p x || q x;
-    compl = p:    x: ! p x;
-    true  = p: true;
-    false = p: false;
-
-    /* predicate "being equal to y" */
-    equal = y:    x: x == y;
-  };
-
-  /* Emulate a "switch - case" construct,
-   instead of relying on `if then else if ...` */
-  /* Usage:
-  ```nix
-  switch-if [
-    if-clause-1
-    ..
-    if-clause-k
-  ] default-out
-  ```
-  where a if-clause has the form `{ cond = b; out = r; }`
-  the first branch such as `b` is true */
-
-  switch-if = c: d: (findFirst (getAttr "cond") {} c).out or d;
-
-  /* Usage:
-  ```nix
-  switch x [
-    simple-clause-1
-    ..
-    simple-clause-k
-  ] default-out
-  ```
-  where a simple-clause has the form `{ case = p; out = r; }`
-  the first branch such as `p x` is true
-  or
-  ```nix
-  switch [ x1 .. xn ] [
-    complex-clause-1
-    ..
-    complex-clause-k
-  ] default-out
-  ```
-  where a complex-clause is either a simple-clause
-  or has the form { cases = [ p1 .. pn ]; out = r; }
-  in which case the first branch such as all `pi x` are true
-
-  if the variables p are not functions,
-  they are converted to a equal p
-  if out is missing the default-out is taken */
-
-  switch = var: clauses: default: with pred; let
-      compare = f:  if isFunction f then f else equal f;
-      combine = cl: var:
-        if cl?case then compare cl.case var
-        else all (equal true) (zipListsWith compare cl.cases var); in
-    switch-if (map (cl: { cond = combine cl var; inherit (cl) out; }) clauses) default;
-})
diff --git a/pkgs/build-support/coq/meta-fetch/default.nix b/pkgs/build-support/coq/meta-fetch/default.nix
index e7b15af4f06e4..c366c0d6a69ab 100644
--- a/pkgs/build-support/coq/meta-fetch/default.nix
+++ b/pkgs/build-support/coq/meta-fetch/default.nix
@@ -1,6 +1,4 @@
 { lib, stdenv, fetchzip }@args:
-let lib' = lib; in
-let lib = import ../extra-lib.nix {lib = lib';}; in
 with builtins; with lib;
 let
   default-fetcher = {domain ? "github.com", owner ? "", repo, rev, name ? "source", sha256 ? null, ...}@args:
@@ -37,7 +35,7 @@ arg:
 switch arg [
   { case = isNull;       out = { version = "broken"; src = ""; broken = true; }; }
   { case = isPathString; out = { version = "dev"; src = arg; }; }
-  { case = pred.union isVersion isShortVersion;
+  { case = preds.union isVersion isShortVersion;
     out = let v = if isVersion arg then arg else shortVersion arg; in
       let
         given-sha256 = release.${v}.sha256 or "";
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index 6490391eb6363..4ff8ccb10edd2 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -5,15 +5,15 @@ mkCoqDerivation {
   pname = "QuickChick";
   owner = "QuickChick";
   defaultVersion = with versions; switch [ coq.coq-version ssreflect.version ] [
-      { cases = [ "8.13" pred.true  ]; out = "1.5.0"; }
-      { cases = [ "8.12" pred.true  ]; out = "1.4.0"; }
-      { cases = [ "8.11" pred.true  ]; out = "1.3.2"; }
-      { cases = [ "8.10" pred.true  ]; out = "1.2.1"; }
-      { cases = [ "8.9"  pred.true  ];  out = "1.1.0"; }
-      { cases = [ "8.8"  pred.true  ];  out = "20190311"; }
+      { cases = [ "8.13" preds.true  ]; out = "1.5.0"; }
+      { cases = [ "8.12" preds.true  ]; out = "1.4.0"; }
+      { cases = [ "8.11" preds.true  ]; out = "1.3.2"; }
+      { cases = [ "8.10" preds.true  ]; out = "1.2.1"; }
+      { cases = [ "8.9"  preds.true  ];  out = "1.1.0"; }
+      { cases = [ "8.8"  preds.true  ];  out = "20190311"; }
       { cases = [ "8.7"  isLe "1.8" ];  out = "1.0.0"; }
-      { cases = [ "8.6"  pred.true  ];  out = "20171102"; }
-      { cases = [ "8.5"  pred.true  ];  out = "20170512"; }
+      { cases = [ "8.6"  preds.true  ];  out = "20171102"; }
+      { cases = [ "8.5"  preds.true  ];  out = "20170512"; }
     ] null;
   release."1.5.0".sha256    = "1lq8x86vd3vqqh2yq6hvyagpnhfq5wmk5pg2z0xq7b7dcw7hyfkw";
   release."1.4.0".sha256    = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc";
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index 4de6e2da8b511..a34aafb803546 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -10,7 +10,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch mathcomp.version [
-    { case = pred.inter (isGe "1.11.0") (isLt "1.13"); out = "1.2.3"; }
+    { case = range "1.11" "1.12"; out = "1.2.3"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp.algebra ];
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 4637edebdb77a..dc125a641dcc5 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -44,7 +44,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 (preds.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/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
index adc4e3a59477b..6c2b5bf117c68 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@@ -10,7 +10,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch mathcomp.character.version [
-    { case = pred.union (isGe "1.10.0") (isEq "dev"); out = "1.12.0"; }
+    { case = range "1.11" "1.12"; out = "1.12.0"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp.character ];
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 1ac8c4c40057e..d8e03922efce6 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -1,7 +1,6 @@
 { lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
 , ocamlPackages_4_10, compcert
 }@args:
-let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
 let
   mkCoqPackages' = self: coq:
     let callPackage = self.callPackage; in {