@Emilio Jesús Gallego Arias I don't quite understand why we need to get rid of minisys from coqdep? Are you suggesting to rely on System? Whats the point of that if System includes Minisys?
We don't need to, what I mean is that it is redundant now
we can just merge minisys into system
before, due to bootstrapping, system couldn't be used
OK merging is what you had in mind
actually we have a lot of weird stuff in these modules that would be great to replace with stdlib / more standard stuff, but that's orthogonal
yup, merging, and actually reducing the surface api there
well I guess merging makes sense, but we can keep both if we want
OK I will merge for now
OK https://github.com/coq/coq/pull/15765
Last updated: Oct 13 2024 at 01:02 UTC