Ltac2: shortest qualid of name

Open JasonGross opened this issue 2 months ago • 4 comments

I would like a version of Env.path that gives me the shortest qualified name that refers to the given reference.

Oct 27 '25 20:10 JasonGross

Why?

Oct 28 '25 07:10 SkySkimmer

I want to write an error message that suggests code to insert in the document. Most people don't write code with fully qualified identifiers.

Oct 28 '25 08:10 JasonGross

Why do you want a qualid instead of printing to message?

Oct 28 '25 08:10 SkySkimmer

I do ultimately want a message. Going through ident list just seems more flexible for possible future users. I'd be fine with something that just gave me a message though

Oct 28 '25 08:10 JasonGross