Rocq Call 2025 05 20 - rocq-prover/rocq GitHub Wiki

• 4pm UTC+2 (Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• ltac2 source code directory structure (https://github.com/rocq-prover/rocq/pull/20650, Gaëtan, 10min)
• future of https://github.com/rocq-prover/rocq/pull/17084 (Gaëtan, 15min)

Roles

• Chairman: Matthieu
• Secretary: Matthieu
• Attending: Matthieu, Gaëtan, PMP

Notes

• ltac2 source code: Agreed to move the .v files to theories/Ltac2, have theories/Corelib (thinking of having theories/Equations in the future).
• future of #17084. Agreed to have a deprecation phase if possible. The feature is good to have.