post-summer synchronization of our directions?

Induction-induction status (Matthieu, 15min)

Ongoing work:

• PMP: cleaning of hints, Ltac2 bugfixes and features (contact with Derek Dreyer and Malecha) Weird behavior of hnf and discrimination nets behavior or meta/evar-closed terms. Maxime suggests commenting the hints code also when we don't understand some pieces of code.

  CUDW doodle to be sent.

• Maxime and Gaëtan: fixing apply and shelf manipulation. 2 directions: continuing on unifall (close to closing 7825) "or" moving goals to the evar_map (solving the advance problem)

• Hugo: working on Notations.

  • Deactivation of notations. PR #12324 RFC for syntax and features also
  • Plan to work on closing PRs:
    • about implicit argument naming
    • Arguments Needs for time to discuss these (CUDW should help here)

• Emilio:

  • Finalizing the work on dune

  • SerAPI and Notations work

  • Later on: document model and scheduling

• Matthieu:

  • Working on ind-ind types. Issue: representation of partial fixpoints during type-checking. If using option body this would naturally give rise to daimon-like values... https://github.com/coq/coq/pull/12464

• Moving to github actions and applying for open-source Gold group-level support (submitted)