affeldt-aist

The last commit makes the dev compile but it is clearly a temporary fix.

> Rebasing the branch over mc-analysis 1.6.0, and in particular over the PR splitting topology in multiple files, makes the compilation fail. `real.v` does not find the splitted files when...

Isn't putting `separation_axioms.v` and `function_spaces.v` in topologies more appropriate? `nat_topology.v` instead of `nats_topology.v`? (since we have `bool_topology.v` among other reasons) (more generally I wonder about the use of plural in...

I noticed a few potential improvements to the documentation in the first conversation item. I do not want to make this a strong requirement for merging: we can always copy-paste...

Some files are names "*_mixin.v", which makes visible to every user a technical term ("mixin") that (I think) we have been trying to substitute by the more general term of...

I agree.

next file is `entropy.v`... :-(

Isn't it rather `cvgMl` that should be `cvgMr` because the constant is on the `r`ight? But then should the current `cvgrM`: ```coq Lemma cvgMr g a b : g @...

We'd better do that after PR #1544 is merged

NB: `cvgeMl` and `cvgeMr` have been renamed by this PR https://github.com/math-comp/analysis/pull/1580