Coq Call 2022 01 26

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

Topics

• https://github.com/coq/coq/pull/11327 (Inherit implicit arguments in coercions)
• collecting, documenting and ideally unifying the various ways to generate inductive schemes (Equations, Elpi, Scheme, ...)
• syntax for setting transparency in Create HintDB (#5381)
• unifall/apply: how to deal with the projection compatibility layer: without delta, compat constant p is not convertible to Proj(p, t) (Matthieu)
• What to do with https://github.com/coq/coq/pull/14777 (Default HintDb) (Ali)
• Hugo wants to discuss focusing our collective efforts on tactics (Ali)
  • We have a lot of tactics, this is confusing for users
  • Adding features to tactics is difficult, no consensus on simplicity vs usability
  • disparity between coq, ssreflect, commonly defined tactics etc.

Notes

• PR 11327: needs more thought, can we avoid entangling parsing/scope interpretation and typing while implementing this feature.
• Schemes: easy to fix the induction tactic lookup thing. A hook for declaring things after the definition of an inductive/constant that is plugin or even user extensible would be enough to handle. Discussion about using namespaces and allowing the nat_rect -> nat.rect change Hugo is proposing. Should be fine if it does not go in conflict with the current namespace CEP.