Stream: Coq devs & plugin devs

Topic: Gensym in kernel for MBIds

view this post on Zulip Maxime Dénès (Mar 08 2022 at 15:35):

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

view this post on Zulip Maxime Dénès (Mar 08 2022 at 15:36):

Is it something that is necessary? When I was a kid, I was told the kernel had a functional interface :)

view this post on Zulip Maxime Dénès (Mar 08 2022 at 15:36):

I suspect @Pierre-Marie Pédrot may know more

Last updated: Dec 01 2023 at 07:01 UTC