affeldt-aist

> For what it's worth, in the proof I have I need to case on the hypothesis to grab the lipschitz clause anyway. Yes, of course. I believe that there...

> we may also consider adding functions and signed there. I would maybe refrain to do so for now because we didn't have (yet?) explicit requests for them and `functions.v`...

what about the near tactic?

i think that at some point it was scheduled to replace bigenough

> Rebased (hope will manage to merge this "soon", because those rebases are rather painful) Agreed. We can maybe merge the easy PRs in the pipeline that touch the relevant...

IIRC, the problem with this PR is that it does not bring the expected code size reduction. But there is now code size augmentation (except with one lemma). Since we...

> (I cannot add [kind: wish] label to this issue. Perhaps because of the lack of permission?) There is maybe something to configure on github's side. I couldn't figure it...

See this comment https://github.com/math-comp/analysis/blob/a6f5faaad30c89779f5e1c3bb70f530e69d5bb71/theories/topology.v#L5728-L5736

Comments partially addressed in PR #572 .

> > So this is the PR that needs linting and refactoring, right? > > Yes, quite heavily. In particular, hahn_banach.v could be transformed in a file depending of mathcomp-analysis,...