Unverified Commit f6371cad authored by Vincent Laporte's avatar Vincent Laporte Committed by GitHub
Browse files

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

parent 7cd68c3d

doc/languages-frameworks/coq.section.md

+6 −11
Original line number Diff line number Diff line
@@ -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"; }

  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 = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }

      { 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;

  };

}

```