Skip to content

Coq Call 2022 03 09

Matthieu Sozeau edited this page Mar 9, 2022 · 5 revisions

Topics

Notes

  • [#15737] Not reconciled views about Ltac2/Ltac. Have to investigate if the proposal for the protocol change by Pierre-Marie and Emilio causes any problem.
  • [#15774] is assigned now
  • Switching CoqIDE to maintenance-only mode: diverging to a roadmap discussion.
    • we lacked planning for the debugger for example and how it integrates with existing work on interfaces.
    • we can discuss again the splitting of coqide if there is a critical mass to take care of maintainance, knowing that labgtk will go away at some point.
Clone this wiki locally