I want to keep an eye on the universe constraints Coq imposes at different steps of a proof. Is there a more convenient way of doing this than adding `Show Universes`

throughout the proof?

no

I find the universes subgraph command helpful, ie `Print Universes Subgraph (prod.u0 list.u0)`

. See also here

Last updated: Jun 23 2024 at 04:03 UTC