[Set Printing All.] does not imply [Set Printing Universes.] about coq HOT 4 OPEN

Note that this is not specific to HoTT/coq, but is also the case in other versions of Coq.

from coq.

This is more or less deliberate. "Set Printing Universes" was
introduced after "Set Printing All". "Set Printing All" does not
include either "Set Printing Existential Instances". It is not clear
to me whether most users want these information in "All", though
certainly this is a misuse of the meaning of "All".

If a consensus emerges for integrating "Universes" and "Existential
Instances" in "All", this is certainly a doable change.

Hugo

On Wed, Feb 20, 2013 at 01:23:36PM -0800, Peter LeFanu Lumsdaine wrote:

Should [Set Printing All.] really mean “all”, or is this a deliberate omission?

—
Reply to this email directly or view it on GitHub.

from coq.

Personally, the main reason I use "Set Printing All" is to figure out why something that looks like it should typecheck doesn't. This isn't usually a universe problem, although with Peter's other issue it might be.

Is "Set Printing Existential Instances" documented anywhere? I can't find it in the reference manual.

from coq.

On Thu, Feb 21, 2013 at 05:04:05AM -0800, Mike Shulman wrote:

Personally, the main reason I use "Set Printing All" is to figure out why
something that looks like it should typecheck doesn't. This isn't usually a
universe problem, although with Peter's other issue it might be.

Is "Set Printing Existential Instances" documented anywhere? I can't find it in
the reference manual.

Indeed not. Thanks for noticing. I just committed a documentation of
it in the main Coq archive.

Hugo

from coq.