Coq Call 2021 01 27 - coq/coq GitHub Wiki

• January 27, 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• Conditional compilation and generated code inside the document (Enrico)

• CEP #49 and PR #11099 (instantiation of non-dependent implicit arguments by name or index): adopting the with model? generalizing it to all (including @foo-style) applied references?

Notes

Mainly free-form discussion of the CEPs