Coq Call 2024 01 29 - coq/coq GitHub Wiki

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.