Coq Call 2022 09 21 - coq/coq GitHub Wiki

Topics

  • Status of VSCoq until new document model/protocol (Karl)
  • RM for 8.17
  • Change of representation of evar instances https://github.com/coq/coq/pull/16442 (PMP)
  • Help speeding up API to demote universes (bottleneck in Elpi)
  • Next steps for a potential renaming? (Théo) (postponed)

Notes

  • Migration plan while we're waiting for the new VsCoq. Ask for a maintainer or help from the community.
  • RM for 8.17
    • Enrico mentions Michael needs help
    • Emergency solution: Théo
  • Representation of evar instances: clients should check if they can get speedups by avoiding expand_existential. Ok with the PR
  • Demoting universes? API questions about universes and multiple declarations