Kazuhiko Sakaguchi

`Makefile` now uses `coq_makefile` three times to provide several build targets and exclude some files from installation. I wish to find an easy way to do this—maybe Dune?

Paramcoq seems broken only in Coq 8.17, but I'm not motivated to investigate it.

Yes, I'm fixing it. While working on the fix, I found that `null_fun` is exported from ~ssralg without the prefix `GRing`~ `GRing.Theory`, which seems wrong to me.

Ok, `\-` (both unary and binary), `\+`, and `\*` notations are defined for ereals in `constructive_ereal.v`, and we need a way to distinguish these notations for rings and ereals. I...

One solution would be to declare `ring_function_scope` and `ereal_function_scope`, which morally work as "subscopes" of `function_scope`, and bind them to two constants representing function types whose codomains are ring and...

This is the current situation, but we may have to revert the renaming. I propose it as a topic for the next meeting: https://github.com/math-comp/math-comp/blob/4281254f5cdc9fe482f11a40011ed44247ddb626/mathcomp/field/falgebra.v#L93-L98

https://github.com/math-comp/math-comp/wiki/Minutes-2024-07-24

To support the case where there are several idempotent elements, the idempotence structure should take `op` as a parameter rather than bundling it.

If the structure I proposed above (semigroup + an idempotent element `idx`) takes `idx` as a type parameter, its instance declaration fixes `idx`. Then, we actually cannot represent a band,...

@proux01 @CohenCyril Can you help me with this? I wanted to make sure that coq/coq#19611 does not break lemma-overloading, and thus, I need to put it back to the CI...