Yves does not think we have time to prepare questions Cyril and Pierre think it is not the right timing. Yves: Can we ask Georges to attend a future meeting? Cyril agrees.

Right now it conflicts with Rocq'n'share. Pierre proposes June 18th or July 2nd. Cyril not available July 2nd

• #1435 : Matteo explains his experiment on monoid.v (see here) where he changes the subject of the structure from the operation to the type. He uses a new feature of HB, namely wrappers that are mixins that contain a factory on a (potentially) different subject. When defining a structure on some subject, we can use the factory on the other subject or the wrapper. Making an instance for one subject or the other declares both instances.
• #1434 : adding modnMDXl, merged
• #1433 : #1256 duplicated some lemmas, this removes the duplicates. A few things get generalized, which makes some coercions non-uniform. Pierre: Let's not care. Cyril asks about the naming changes (zmod_closedD -> zmod_closed0D and subr_2closed -> subr_closed).
• #1420 : Cyril's first review was fixed, he is doing a second review.

Cyril