Quentin VERMANDE comments

Results 98 comments of


                                            Quentin VERMANDE

Move the definitions of archimedean structures from ssrnum.v to archimedean.v

If you are ready, I think you can ignore us and I will rebase when you merge.

adherence value, extracted seq, limit point

> Note that Bolzano-Weierstrass is a direct consequence of these lemmas. How so?

Generalize integration_by_parts

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

Instances on function types

There is still half of https://github.com/rocq-prover/rocq/pull/19822 that needs to be done before we can have instances on dependent function types and it would be sad to do things only for...

Holomorphy

What should I do about the lemmas I put in `unstable.v` that require `real-closed`?

rm problematic variables under evars for evar instantiation

I am not sure what to do about `bug_3209.v`. It seems the problem it describes disappears with this PR. I expect we would not want to get rid of the...

rm problematic variables under evars for evar instantiation

I fail to reproduce the `argosy` issue (even after rebasing).

rm problematic variables under evars for evar instantiation

@ppedrot I can compile both minimizations... But I could reproduce the argosy issue (I had already done an overlay but never pushed it for some reason).