Stream: Coq devs & plugin devs

Topic: Vernacular commands and Gallina types

view this post on Zulip Guillaume Melquiond (Feb 11 2021 at 19:33):

I have a custom vernacular command that eventually does stuff depending on a type. Currently, I am doing Stdarg.wit_ref -> Constrintern.locate_reference -> Typeops.type_of_global_in_context. But that feels clumsy. What is the best approach?

Last updated: Dec 05 2023 at 06:01 UTC