Coq Call 2021 07 13 - coq/coq GitHub Wiki

• July 13th 2021, 4pm-5pm Paris Time (NB: the date is not a typo, this is on Tuesday as the 14th is a French holiday)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Discuss user-defined rewrite rules CEP #50. (Ali Caglayan, on behalf of Theo).
• Stuck debugger PR #14354. See the comment here. (Jim Fehrle)

Notes

• Everyone's fine with 6137
• User-defined rewrite rules
  • removes dependency on private inductive types
  • no big obstacle, only we're missing a candidate implementer
  • Gaëtan might be interested
• Let's sync on Coq for away times in summer
• 8.14 issues: dune/install issues mainly, Emilio is still on them.
• Jim's PR: apparently needs another round

Postponed

• preliminary evaluation of coqnative (Emilio J. Gallego Arias)