• 16:00 UTC+1:00 (CET, Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• ssreflect rewrite -> rw and addition to prelude ( https://github.com/rocq-prover/rocq/pull/21478 , Pierre, 15 min)
• if-then-else syntactic sugar ( https://github.com/rocq-prover/rocq/pull/21609 , Pierre, 25 min)
• Good Defaults (https://github.com/rocq-prover/rocq/pull/19117, Théo(s), 10 min)

Roles

• Chairman: Matthieu Sozeau
• Secretary: Enrico Tassi
• Attending: Enrico Tassi, Matthieu Sozeau, Andres Erbsen, Théo Winterhalter, Pierre Roux, Gaëtan Gilbert, Yann Leray

Notes

"rw" #21478

• rw avoids conflicts

  • CI almost all green

• GG: first rename, then add to prelude / fix conflicts

• PR: will do the split

"if-t-e" #21609

• ALL: standard if relies on the orders of constructors, we should deprecate it (unless the type is bool)

• of course we do not converge, many proposals, we make a poll in zulip

• CC: please no opt-in, we pick one one and is on by default so that everybody uses it

• PR: will do the poll

defaults #19117

• GG: proposes Type Class Default Mode

• CC: hint opaque is global, hence contaminating: two different logic programs (Ttype Classes) may need different settings

• PMP, GM: the PR does things the wrong way, it should change the default and put in Compat.v the wrong (old) default