Assia Mahboubi
Assia Mahboubi
Indeed, this third variant was missing... thanks! If I remember correctly, @thery wrote his own in `alt.v`... It seems to me though that the present proof is going into some...
See [this line](https://github.com/math-comp/analysis/blob/3edd010fa7b101f449c6f364e0dfacb51b546496/theories/cauchyetoile.v#L196), for topological zmodtype.
- [ ] ~~Obtain axioms from the std library~~ Keep the explicit list of additional axioms, and derive their standard consequences. - [x] Remove ugly notation for `asbool` - [x]...
For now it is not clear how to proceed: is it broken or is documentation missing? Many lines in [this](https://github.com/math-comp/analysis/blob/3edd010fa7b101f449c6f364e0dfacb51b546496/theories/cauchyetoile.v#L194) file declare instances for C^o, using its convertibility with C...
Remove the level of subsections in the TOC at the beginning.
End of section 8.4 , in the definition of `pack` : provide a type annotation for `m` and explain why `m0` cannot be used as such, as in `Pack (@Class...
See example in section 8.3. For the sake of uniformity, I have removed it from the inline. It is more uniformly uglier.
We use it in section 8.1. I have added a sentence but more might be needed.
The 1st paragraph in section 8.1 is not clear: clarify the discourse about structure vs interface.
As Simon says, the block of notations declarations (LHS, etc) is too dry and deserves a line-per-line comment.