Skip to content

Coq Call 2019 10 23

Théo Zimmermann edited this page Jan 9, 2020 · 2 revisions

October 23rd at 4pm Paris time. Add topics you would like to see discussed.

Topics (from last time & new)

  • Duplication of the parsing state (system and parsing in Vernacstate.t) (Maxime, if Emilio is present)
  • CEP #40: where to put the proofs? (Enrico, with Pierre-Marie, if Emilio is present)
  • Coq 8.10.1
  • Release cycle duration from the user point of view (Théo)

Notes:

  • We should provide example fixes for the upcoming breaking changes in 8.11 (e.g. Export bug)
  • 8.10.1 should be released ASAP with the SProp soundness bug and more fixes
  • Discussion around globref / projections cleanup. Shall we have a higher level notion for names including projection names?
Clone this wiki locally