{
  lib,
  mkCoqDerivation,
  coq,
  mathcomp,
  stdlib,
  version ? null,
}:

mkCoqDerivation {
  pname = "reglang";

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

  release."1.2.2".sha256 = "sha256-js1JaLSpYbxfiAfh8XvGsnJpx5DV13heouUm3oeBfNg=";
  release."1.2.1".sha256 = "sha256-giCRK8wzpVVzXAkFAieQDWqSsP7upSJSUUHkwG4QqO4=";
  release."1.2.0".sha256 = "sha256-gSqQ7D2HLwM4oYopTWkMFYfYXxsH/7VxI3AyrLwNf3o=";
  release."1.1.3".sha256 = "sha256-kaselYm8K0JBsTlcI6K24m8qpv8CZ9+VNDJrOtFaExg=";
  release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk=";

  inherit version;
  defaultVersion =
    let
      case = coq: mc: out: {
        cases = [
          coq
          mc
        ];
        inherit out;
      };
    in
    with lib.versions;
    lib.switch
      [ coq.coq-version mathcomp.version ]
      [
        (case (range "8.16" "9.1") (range "2.0.0" "2.5.0") "1.2.2")
        (case (range "8.16" "9.0") (range "2.0.0" "2.3.0") "1.2.1")
        (case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "1.2.0")
        (case (range "8.10" "8.20") (isLt "2.0.0") "1.1.3")
      ]
      null;

  propagatedBuildInputs = [
    mathcomp.ssreflect
    stdlib
  ];

  meta = {
    description = "Regular Language Representations in Coq";
    maintainers = with lib.maintainers; [ siraben ];
    license = lib.licenses.cecill-b;
    platforms = lib.platforms.unix;
  };
}