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

compcert: enable for Coq 9.0.1 & default to Coq 9.0 (#447163)

parents 9e538263 d1d4809b

pkgs/development/coq-modules/compcert/default.nix

+13 −0
Original line number Diff line number Diff line
@@ -303,6 +303,19 @@ let 
              })

            ];

          }

          {

            cases = [

              (isEq "9.0")

              (isEq "3.16")

            ];

            out = [

              # Support for Coq 9.0.1

              (fetchpatch {

                url = "https://github.com/AbsInt/CompCert/commit/a962ef9da0fb4ef2a4314ccedd111eb248e42cf2.patch";

                hash = "sha256-ipYqcfcgz3cKyI1NGSgfOgiVdV1WUwlv6DVB1S1hJvw=";

              })

            ];

          }

        ]

        [ ];

  });

pkgs/top-level/all-packages.nix

+1 −1
Original line number Diff line number Diff line
@@ -4598,7 +4598,7 @@ with pkgs; 
    ocamlPackages = ocaml-ng.ocamlPackages_4_14;

  };



  inherit (coqPackages_8_20) compcert;

  inherit (coqPackages_9_0) compcert;



  computecpp = wrapCCWith rec {

    cc = computecpp-unwrapped;