Coq Call 2019 10 23 - coq/coq GitHub Wiki

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?