Stream: Coq devs & plugin devs

Topic: Printing terms with longest qualid.


view this post on Zulip Thomas Reichel (Mar 13 2023 at 07:52):

Hi all, I know that Locate can look up the full (longest) qualid/path of something in the environment, but I'd also like to be able to Print a term using only full qualids/paths in the output. What would be the easiest way to do this in a plugin? At least under my cursory inspection it doesn't look like it's possible to convince the existing printers to do this. Thanks!

view this post on Zulip Hugo Herbelin (Mar 14 2023 at 22:23):

There is at least a hackish way to do it (I don't how much other devs would be ok to recommend it): it is to use Constrextern.set_extern_reference to set the printer you want (typically Nametab.full_name_cci in place of Nametab.shortest_qualid_of_global, I guess).

Otherwise, we may also add a new option, say Set Printing Fully Qualified. to specifically print references fully qualified in Constrextern.default_extern_reference and make a PR for it.


Last updated: Jun 09 2023 at 07:01 UTC