Kazuhiko Sakaguchi comments

Results 306 comments of


                                            Kazuhiko Sakaguchi

Port to `HB.lock`

`T` in `{fset T}` is not interpreted in `type_scope` anymore. I will fix it. (It would be better if we address math-comp/math-comp#1136 though.)

> `T` in `{fset T}` is not interpreted in `type_scope` anymore. I will fix it. (It would be better if we address [math-comp/math-comp#1136](https://github.com/math-comp/math-comp/issues/1136) though.) Fixed.

Fix

Coq-community templates regenerated `resources/index.md`, but I'm unsure if that's what we want. Anyway it looks unmaintained.

automate opam release

I would rather discontinue Algebra Tactics in its current form (and remove it from Rocq Platform) since @proux01 is porting it to the main MathComp repo. Then, I may want...

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

~I will add a commit to address #1236 later.~ Done.

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

@affeldt-aist Can you take a look at analysis?

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

@affeldt-aist I'm rather asking for a fix because we already know that analysis is broken (see CI).

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

@affeldt-aist I added your PR as an overlay but analysis is still broken.

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

@affeldt-aist Yes, but that was deprecated in MathComp 2.1.0.

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

I still need to remove `Qint`, `Cint`, etc., and change at least Abel and Apery accordingly.