Attending: Yves, Pierre, Cyril, Enrico, Kazuhiko

• Progress on bugs found during the finmap sprint:

  • DONE: https://github.com/coq/coq/pull/18705 / excess of reversible coercions
  • DONE: https://github.com/coq/coq/pull/18712 / evarconv extraargs bug

• News from the finmap coding sprint:

  • Bug affecting bigop.v seems to be solved in recent commit by GG.
  • Cyril will try to port finset.v by the next meeting
  • The long comment in finpred suggests a custom search procedure should not allow to mistake the LHS and RHS (in unification they are both terms and when doing recursive calls one may flip, but the search procedure unfolds on one side first, not the other, so it is not symmetric)

• Pierre and Reynald looked at issue 1170 (https://github.com/math-comp/math-comp/pull/1179)

  • after a live discussion on various options, Pierre will try to apply a solution from ssrnum (a Def module)

• splitting order.v into subfiles / its own mathcomp-order package?

  • first two PRs should be merged, then we can consider this
  • proposed chunks: lattices, partial order, total order + morphisms distributed inside these
  • we could use NES to coalesce into a single Order name space the ones that come from single files (right now there is a single Order module in the single order.v file, so users do Order.le for example, we don't want to break these)