Coq Call 2022 04 06 - coq/coq GitHub Wiki

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

Topics

• Move universe inference out of kernel (https://github.com/coq/coq/pull/15890)
• InferCumul treats definitions as invariant except if asked explicitly (https://github.com/coq/coq/pull/15662)

Notes

• PR 15890: Ok with the patch

• PR 15662: ok with the new heuristic, we don't have to provide the old unscalable complete unfolding strategy yet.

• OCaml version bump: 4.08 or 4.09 or 4.11 ?

  4.10 to 4.13 are bad for us actually. 4.09 seems fine.