doc: clean-up Coq derivation example (#299927)

1 files changed, 6 insertions, 11 deletions

diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md
index db3724773345..fdc824781cd1 100644
--- a/doc/languages-frameworks/coq.section.md
+++ b/doc/languages-frameworks/coq.section.md
@@ -56,22 +56,17 @@ Here is a simple package example. It is a pure Coq library, thus it depends on C
 { lib, mkCoqDerivation, version ? null
 , coq, mathcomp, mathcomp-finmap, mathcomp-bigenough }:
 
-let
-  inherit (lib) licenses maintainers switch;
-  inherit (lib.versions) range;
-in
-
 mkCoqDerivation {
   /* namePrefix leads to e.g. `name = coq8.11-mathcomp1.11-multinomials-1.5.2` */
   namePrefix = [ "coq" "mathcomp" ];
   pname = "multinomials";
   owner = "math-comp";
   inherit version;
-  defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
-      { cases = [ (range "8.7" "8.12")  "1.11.0" ];             out = "1.5.2"; }
-      { cases = [ (range "8.7" "8.11")  (range "1.8" "1.10") ]; out = "1.5.0"; }
-      { cases = [ (range "8.7" "8.10")  (range "1.8" "1.10") ]; out = "1.4"; }
-      { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
+      { cases = [ (range "8.7" "8.12") (isEq "1.11") ];        out = "1.5.2"; }
+      { cases = [ (range "8.7" "8.11") (range "1.8" "1.10") ]; out = "1.5.0"; }
+      { cases = [ (range "8.7" "8.10") (range "1.8" "1.10") ]; out = "1.4"; }
+      { cases = [ (isEq "8.6")         (range "1.6" "1.7") ];  out = "1.1"; }
     ] null;
   release = {
     "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s";
@@ -90,7 +85,7 @@ mkCoqDerivation {
 
   meta = {
     description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
-    license = licenses.cecill-c;
+    license = lib.licenses.cecill-c;
   };
 }
 ```