diff options
| author | Vincent Laporte <vbgl@users.noreply.github.com> | 2024-03-31 19:35:35 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2024-03-31 10:35:35 -0700 |
| commit | f6371cad747aef21cac3829ab050865b47806de0 (patch) | |
| tree | a5852c029e54f7a40af8f7ad93e8579925f18c7d /doc | |
| parent | 7cd68c3dc8260a107a32f532a648e5ec32fbfe75 (diff) | |
doc: clean-up Coq derivation example (#299927)
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/languages-frameworks/coq.section.md | 17 |
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; }; } ``` |