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: Feb 04 2023 at 01:03 UTC