Ltac2: shortest qualid of name

[JasonGross]

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

[SkySkimmer]

Why?

[JasonGross]

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.

[SkySkimmer]

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

[JasonGross]

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