lol
at 25.11-pre 43 lines 859 B view raw
1{ 2 coq, 3 mkCoqDerivation, 4 mathcomp-boot, 5 lib, 6 version ? null, 7}: 8 9mkCoqDerivation { 10 11 namePrefix = [ 12 "coq" 13 "mathcomp" 14 ]; 15 pname = "bigenough"; 16 owner = "math-comp"; 17 18 release = { 19 "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg"; 20 "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"; 21 "1.0.2".sha256 = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0="; 22 }; 23 inherit version; 24 defaultVersion = 25 with lib.versions; 26 lib.switch coq.version [ 27 { 28 case = range "8.10" "9.0"; 29 out = "1.0.2"; 30 } 31 { 32 case = range "8.5" "8.14"; 33 out = "1.0.0"; 34 } 35 ] null; 36 37 propagatedBuildInputs = [ mathcomp-boot ]; 38 39 meta = { 40 description = "Small library to do epsilon - N reasonning"; 41 license = lib.licenses.cecill-b; 42 }; 43}