Rocq Call 2025 04 29 - rocq-prover/rocq GitHub Wiki

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

Topics

• Decide what to do for tactics like transitivity needing a parsing rule in Ltac2 (Thomas, 20-30 min) See this PR or these discussions on zulip #Ltac2 > stdlib notations and #Rocq devs & plugin devs > Port stdlib to Ltac2?

Roles

• Chairman:
• Secretary:
• Attending:

Notes