I normally applaud any Coq porting efforts, but now we have two diverging/incomparable High School Geometry: https://github.com/thery/HighSchoolGeometry https://github.com/coq-contribs/high-school-geometry (see here for context). Not sure what to do?

Agreed with you: the best would be to decide that @thery's version become the official one and the coq-contrib be archived and redirect to the other.

I wonder if some day we need internationalization for Coq files - also some of the Coquelicot examples are not easy to understand with rusted French

Last updated: Jun 06 2023 at 23:01 UTC