Coq Call 2023 01 04 - coq/coq GitHub Wiki

:confetti_ball: Happy new year! :confetti_ball:

• January 4th 2023, 4pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Organization of the Coq Working Group on January 31st/February 1st? (Matthieu, 5min)
• https://github.com/coq/coq/pull/16903 "Introduce sort variables in unification", CEP (PMP)
• "Back"/"Undo" don't undo syntax extensions" (E. Gallego Arias: I've added this, however I will likely miss the call due to being still in holidays, but maybe other devs can discuss about it as it is an extremly critical bug for IDEs)

Notes

• Coq WG January 31st/February 1st, we need to book a room (Hugo or Emilio?)
• Sort variables. Mergeable, once we choose a debug printing option (syntax is not fixed at this point, so it won't be parseable).
• Back/Undo: needs more investigation