affeldt-aist

Maybe we could put this to the agenda of the next meeting? (2023-11-08)

I have just reported a few comments that were made during today's meeting + alpha but maybe I should have addressed most of them myself directly. I'll try to do...

Compilation fails in `galois.v`. I am afraid I am missing something.

HB comes with Hiearchy-builder https://github.com/math-comp/hierarchy-builder this is a requirement for MathComp 2 you can certainly install everything by hand just look at the opam files in each repo to track...

> The new interval stuff may be cleaner here. And I am worried about legibility if we have to add these [measure of ] annotations to every term. Note that...

One year ago this PR introduced the Bernoulli probability measure. The main problem pointed at in particular by @zstone1 was that the definition was not very readable. It was using...

fyi: @proux01 @hoheinzollern (comments also welcomed if you have time)

I still have to move a few things around and to make the changelog and the doc but I think that it addresses the comments from the last meeting, mainly...

@hoheinzollern @t6s the PR is now complete (with changelog and doc)

the merged PR #1142 provides a quick fix but that file maybe deserves to be updated and moved to master, so I keep the issue open