I (re)discovered we have a gensym for module bound identifiers in the kernel : https://github.com/coq/coq/blob/master/kernel/names.ml#L203
Is it something that is necessary? When I was a kid, I was told the kernel had a functional interface :)
I suspect @Pierre-Marie Pédrot may know more
Last updated: Dec 01 2023 at 07:01 UTC