Pierre Roux (chair), Cyril Cohen (secretary), Reynald Affeldt, Alessandro Bruni, Matteo Calosci, Enrico Tassi, Quentin Vermande.

Diverging opinions: https://github.com/rocq-prover/rfcs/pull/108

• Enrico's proposal: just have feedback as a warning, no need to give meaning to bullets or whitespaces. Ok both for people who want to give no semantics and those who want to enforce it.

• Rocq warnings are configurable. In mathcomp we can warn in interactive mode and error at compilation time.

• Some people find the by annoying to edit.

• Cyril's proposal: expose the state of the ssreflect proof engine so we know what happens at each stage. e.g. by rewrite A B C., move=> {x}, rewrite A B C in x y z *...

Forgotten PR, merged.

https://github.com/math-comp/math-comp.github.io/pull/113#issuecomment-3008108193

Decision: ask the authors what they think.

Tentative documentation meeting on July 16th, 9:00-11:00.