Attendees: Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Enrico Tassi, Cécile

#1338 is still broken because of an issue with interval_inference.

We will probably merge #1513 knowing that the new structures will change. Cyril will take care of it.

Rocq PR: https://github.com/rocq-prover/rocq/pull/21478

Introduction of Ssreflect rw to Prelude.v breaks a few things.

• bullet, indentation, controling number of resulting goals... (again)
• Renaming GRing.exp (#1503)
• PR triage

Next meeting on January 21st. Cyril volunteers.