Attendees : Reynald Affeldt, Cyril Cohen, Cécile Marcon, Pierre Roux, Kazuhiko Sakaguchi, Quentin Vermande

We decided to rename exp into pow so that we can name exp the exponential function in MCA. Reynald implemented it. There are several issues. There is expR for the real exponential, expeR for the extended reals, powR for the power function but that does not behave as expected with negative numbers, and poweR for the extended reals (draft PR). There is also GRing.exp, we decided to use pown, is the n in pown pointing to the exponent or is it a fixed name, i.e. is it part of the Québec notation or not? One strategy could be to distinguish between the 1-argument functions (exp) and the 2-argument ones (pow). Another would be to distinguish between homogeneous power functions and heterogeneous ones, i.e. the ones with the same type for the base and exponent and the others. We probably want to systematically annotate with the type of the arguments. The nat -> nat -> nat one is special because of bootstrapping issues but all the others come from the structure of the base. We reach the following naming:

• powrMz : x ^ (n * m) (with n m : int)
• powrMn : x ^ (n * m) (with n m : nat)
• pow1rn : 1 ^+ n
• powMrn : (x * y) ^+ n
• powrMn_n : (x *+ n) ^+ m
• pow0rn : 0 ^+ n
• powrDn : x ^+ (n + m)
• powDrn : (x + y) ^+ n Let us only do renaming for now, without introducing more stuff and do things incrementally using the CI to catch issues as quickly as possible. Reynald will do it. Cyril and Reynald do not want complicated conversations in the PR, using the meeting for discussions.

Side note, seq should be renamed list, quickly.

We can move ordered nmodules and ordered zmodules to order as well.

35 very small overlays. People write *) in Rocq code, which breaks the parsing of ssreflect. There are a few overlays for the is and of keywords. A few libraries use the _foo_ pattern. Pierre wants to use __foo__ but it is longer. Maybe UTF8 characters. There are a few pose ltac:(bla) which get parsed as pose ltac : bla.

HB.about broken too. Cécile volunteers.

Pierre and Quentin will be there. Quentin will announce it.

Pierre