coqPackages.vcfloat: init at 2.1.1

{ lib, mkCoqDerivation, coq, interval, compcert, flocq, bignums, version ? null }:

with lib; mkCoqDerivation {

  pname = "vcfloat";

  owner = "VeriNum";

  inherit version;

  defaultVersion = with versions; switch coq.coq-version [

    { case = range "8.16" "8.17"; out = "2.1.1"; }

  ] null;

  release."2.1.1".sha256 = "sha256-bd/XSQhyFUAnSm2bhZEZBWB6l4/Ptlm9JrWu6w9BOpw=";

  releaseRev = v: "v${v}";

  propagatedBuildInputs = [ interval compcert flocq bignums ];

  meta = {

    description = "A tool for Coq proofs about floating-point round-off error";

    maintainers = with maintainers; [ quinn-dougherty ];

    license = licenses.lgpl3Plus;

  };

}

      tlc = callPackage ../development/coq-modules/tlc {};

      topology = callPackage ../development/coq-modules/topology {};

      trakt = callPackage ../development/coq-modules/trakt {};

      vcfloat = callPackage ../development/coq-modules/vcfloat {};

      Velisarios = callPackage ../development/coq-modules/Velisarios {};

      Verdi = callPackage ../development/coq-modules/Verdi {};

      VST = callPackage ../development/coq-modules/VST ((lib.optionalAttrs