Commit 1be419de authored by Pierre Roux's avatar Pierre Roux Committed by Vincent Laporte
Browse files

coqPackages.mathcomp-analysis: rename altreals to experimental-reals 

Following
https://github.com/proux01/analysis/pull/new/experimental-reals
parent d363c5f2

pkgs/development/coq-modules/mathcomp-analysis/default.nix

+4 −3
Original line number Diff line number Diff line
@@ -54,7 +54,7 @@ let 
  packages = {

    "classical" = [];

    "reals" = [ "classical" ];

    "altreals" = [ "reals" ];

    "experimental-reals" = [ "reals" ];

    "analysis" = [ "reals" ];

    "reals-stdlib" = [ "reals" ];

    "analysis-stdlib" = [ "analysis" "reals-stdlib" ];
@@ -62,12 +62,13 @@ let 


  mathcomp_ = package: let

      classical-deps = [ mathcomp.algebra mathcomp-finmap ];

      altreals-deps = [ mathcomp-bigenough ];

      experimental-reals-deps = [ mathcomp-bigenough ];

      analysis-deps = [ mathcomp.field mathcomp-bigenough ];

      intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});

      pkgpath = lib.switch package [

        { case = "single"; out = "."; }

        { case = "analysis"; out = "theories"; }

        { case = "experimental-reals"; out = "experimental_reals"; }

        { case = "reals-stdlib"; out = "reals_stdlib"; }

        { case = "analysis-stdlib"; out = "analysis_stdlib"; }

      ] package;
@@ -81,7 +82,7 @@ let 
        propagatedBuildInputs =

          intra-deps

          ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps

          ++ lib.optionals (lib.elem package [ "altreals" "single" ]) altreals-deps

          ++ lib.optionals (lib.elem package [ "experimental-reals" "single" ]) experimental-reals-deps

          ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps;



        preBuild = ''

pkgs/top-level/coq-packages.nix

+1 −1
Original line number Diff line number Diff line
@@ -99,12 +99,12 @@ let 
      mathcomp-character = self.mathcomp.character;

      mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel {};

      mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics {};

      mathcomp-altreals = self.mathcomp-analysis.altreals;

      mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};

      mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib;

      mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery {};

      mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};

      mathcomp-classical = self.mathcomp-analysis.classical;

      mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals;

      mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {};

      mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo {};

      mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};