Karl Palmskog (Jul 02 2020 at 12:31): Karl Palmskog (Jul 02 2020 at 12:31):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?
Théo Zimmermann (Jul 02 2020 at 15:38):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.
Michael Soegtrop (Jul 04 2020 at 10:31):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