Participants: Reynald, Cyril, Marie, Yves, Enrico, Laurent, Christian

• PR 599 (apply, dup, swap)
  • Cyril had another idea for the case for [dup] where the duplicated assumption is a proof variable (seems not to work though).
  • PR still needs review
  • care should be taken, because this will become part of Coq once merged
  • conclusion: Create PR for Coq to see if anything breaks.
  • Documentation for the Coq rererence manual is still needed
• PR 501( /[inE], /[mxE] )
  • syntax is still not finalized (/inE vs /[inE] vs /[!inE] ... )
  • needs further offline discussion (Cyris, Enrico, Maxime)
• mathcomp topic on GitHub
  • everyone agrees this useful
  • Enrico agrees to create the PR on the GitHub repo for this
• Reynals wants the Zulip bot to publish website updates
  • should not be mixed with Repository events (which many people have switched off)
  • needs a new webhook; Cyril agrees to have a look into it
• Next Release (mathcomp-1.12)
  • 20 open issues/PRs milestoned
  • tentatively scheduled for end of November
  • need second release manager (first will be Reynald, second should be agreed upon in the next meeting)
  • need to check whether the latest release is compatible with upcoming coq-8.13 (wait until there is v8.13 branch, scheduled for mid November)
• (External) PR reviewers
  • reviewers need to be invited to the math-comp organization
  • this can only be done by the owners
• Cyril wants to make progress towards PR 207
  • this needs (considerable) reviewing power