Rocq Call 2025 07 01 - rocq-prover/rocq GitHub Wiki

• 16:00 UTC+2:00 (CEST, Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• deprecating legacy attribute Local, Global (Pierre, 15min)
  • There are pros and cons, but I think that attribute use is going to go up over time, so I view this as modernization. (Gregory)
• using keyword Abbreviation instead of Notation for abbreviations (Pierre, 15min)
• locality of abbreviations, c.f. #20816 (Pierre, 15min)
• https://github.com/rocq-prover/rocq/pull/20813 (PMP)
• discussing indentation based bullet behavior RFC#108 (Pierre, 15 min, time permitting)

Roles

• Chairman: Nicolas
• Secretary: Matthieu
• Attending: P. Roux, T. Zimmermann, Y. Bertot, E. Tassi, P. Rousselin, Y. Leray, G. Malecha

Notes

• Deprecation of Local/Global. Wait for attributes to be more widely used and revisit that question.
• Abbreviation for Notation: ok.
• locality of abbreviations: properly implement local/global/export for abbreviations, default (export) behavior should be the fixed one and global close to current behavior
• PR #20813: ok for the change.
• Indentation-based bullets: to be discussed with the math-comp team.