doc & changelog

Author: affeldt-aist

.nix/config.nix

@@ -42,36 +42,34 @@ in {
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "9.1";
+  default-bundle = "9.1-master";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
 
-  bundles."9.0-2.5.0" = {
-    rocqPackages = {
-      rocq-core.override.version = "9.0";
-      mathcomp.override.version = "2.5.0";
-    };
-    coqPackages = common-bundle // {
-      coq.override.version = "9.0";
-      mathcomp.override.version = "2.5.0";
-    };
-  };
-
-  bundles."9.0" = {
+  bundles."9.0-master" = {
     rocqPackages = {
       rocq-core.override.version = "9.0";
+      mathcomp.override.version = "master";
+      mathcomp-bigenough.override.version = "master";
+      mathcomp-finmap.override.version = "master";
+      micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.0";
+      ssprove.job = false;  # not yet available for 9.1
     };
   };
 
-  bundles."9.1" = {
+  bundles."9.1-master" = {
     rocqPackages = {
       rocq-core.override.version = "9.1";
+      mathcomp.override.version = "master";
+      mathcomp-bigenough.override.version = "master";
+      mathcomp-finmap.override.version = "master";
+      micromega-plugin.override.version = "master";
     };
     coqPackages = common-bundle // {
       coq.override.version = "9.1";
@@ -85,8 +83,6 @@ in {
       stdlib.override.version = "master";
       rocq-elpi.override.version = "master";
       hierarchy-builder.override.version = "master";
-      micromega-plugin.override.version = "master";
-      micromega-plugin.job = false;
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
       mathcomp-finmap.override.version = "master";

CHANGELOG_UNRELEASED.md

@@ -96,6 +96,9 @@
 - in `reals.v`:
   + lemmas `sup_ge0`, `has_sup_wpZl`, `gt0_has_supZl`, `has_sup_Mn`, `sup_Mn`
 
+- in `lebesgue_stieltjes_measure.v`:
+  + definition `lebesgue_display`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

theories/lebesgue_measure.v

@@ -338,7 +338,6 @@ End LebesgueMeasure.
 
 Definition lebesgue_measure {R : realType} : set R -> \bar R :=
   lebesgue_stieltjes_measure idfun.
-Check fun R : realType => lebesgue_stieltjes_measure idfun : Measure.type _ _.
 HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
   SigmaFiniteMeasure.on (@lebesgue_measure R).

theories/lebesgue_stieltjes_measure.v

@@ -33,6 +33,10 @@ From mathcomp Require Import realfun.
 (*         R.-ocitv.-measurable == semiring of sets of open-closed intervals  *)
 (*                  wlength f A := f b - f a with the hull of the set of real *)
 (*                                 numbers A being delimited by a and b       *)
+(*           @measurableTypeR R == measurableType generated by R.-ocitv       *)
+(*          @lebesgue_display R == (measure_)display for the sigma-algebra    *)
+(*                                 generated by R.-ocitv                      *)
+(*               @measurableR R == measurable sets generated by R.-ocitv      *)
 (* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f           *)
 (*                                 f is a cumulative function.                *)
 (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *)
@@ -522,7 +526,7 @@ Definition measurableR : set (set R) :=
 HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) :=
    Measurable.on (measurableTypeR R).
 (* Presumably it is safe to use NFI here because morally R is unique
-   and nothing else can be used here*)
+   and nothing else can be used here *)
 #[non_forgetful_inheritance]
 HB.instance Definition _ := Measurable.copy R (measurableTypeR R).