feat(print): prefix each printed object with its `locate' report

[bgregoir]

print' resolves a name to one object and shows its declaration, saying nothing about which of the homonyms in scope that was. It now prefixes each object it displays with the report locate' gives for it -- the name the object is known under, and the shortest form that still resolves to it:

print op (+).

(* Int.(+) (shorten name: (+)) *)
abbrev (+)  : int -> int -> int = CoreInt.add.

The computation lives in EcPrinting.locate_path', which both commands now share, so the two cannot drift apart. ObjectInfo.pr_ty', pr_op' and pr_ax' take ?locate', and pr_any' turns it on for those three categories; the others (theories, modules, procedures, module types) get no report, as `locate' knows nothing about them.

A name with no namespace prefix says nothing the declaration does not, and is left out -- the convention the `~long' flag of the declaration printers already followed, and which the report supersedes.

Names are spelled the way the category at hand spells them, through the new ?pp_name' of pp_locate_path': an operator needs its parentheses back to be valid syntax, so the report reads Int.(+)', not Int.+'.

Along the way:

• locate' on an unknown name printed an empty line. The message was written to the formatter after the only flush, so it never reached the buffer notify' reads.

• print' on an unknown name now names it, and ends on a blank line like the successful printers do: "no object x' in the category [...]" instead of "no such object in the category [...]".