Rocq Call 2025 07 01
- 16:00 UTC+2:00 (CEST, Paris time zone offset)
- https://rendez-vous.renater.fr/rocq-call
- 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
Abbreviationinstead ofNotationfor 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)
- Chairman: Nicolas
- Secretary: Matthieu
- Attending: P. Roux, T. Zimmermann, Y. Bertot, E. Tassi, P. Rousselin, Y. Leray, G. Malecha
- 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.
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.