Future plans - rocq-prover/rocq GitHub Wiki

Ongoing work:

• Inductive-inductive types / recursive-recursive functions (Matthieu Sozeau)

  https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Induction.20induction

• UIP / Lean importer (Gaëtan Gilbert)

• Ltac2 (Pierre-Marie Pédrot)

• VSCoq / IDEs (Maxime Dénès, Enrico Tassi, ...)

• stdlib2 (Maxime Dénès, ...)

• Refactorings / functionalization of proof handling, global declarations (Emilio Jesus Gallego Arias)

• dune (Emilio Jesus Gallego Arias, ...)

• The Coq Platform (Michael Soegtrop)

• Persistent arrays (Maxime Dénès, Benjamin Grégoire)

• Reference manual restructuring + improvements (Théo Zimmermann, Jim Fehrle...) Refman improvements in 8.12 and beyond