Coq Call 2024 01 29

• January 29th (Monday!), 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• We do want to remove the distinction between folded and unfolded primitive projection, right? E.g., what do we want unfold p or cbv delta [p] to mean if p is a primitive projection? (see e.g. #18578) (Hugo, 5-20 min)
• Do we want a strong enforcement of simpl never in simpl, even if it induces some incompatibilities, as shown in #18581? (Hugo, 5-10 min)
• A round about long-standing pull requests looking for assignee? (5-30 min)

Roles

• Chairman: Nicolas Tabareau
• Secretary:

Notes

• Hugo has proposed to work on removing the flag for the unfolding of primitive projections to get a uniform behavior
• simpl never needs to be documented to explain that it holds at top-level but not when reducing arguments of a destructor.