The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hello,

On 06/09/18 13:55, Jan-Oliver Kaiser wrote:

> You can print entire modules using [Print] or [Print Module] in case of 
> ambiguities.

Thank you, I simply hadn't thought of that. Pretty useful.

> Apart from that, [Set Printing Universes] should *sometimes* show the
> full universe cycle when an inconsistency occurs, but it depends very
> much on the particular error that appears.

This I find very interesting. Could someone with insight into the
algorithm comment on which kind of type checking problems are more
likely to trigger an error message providing a full cycle?

Other than that, has anyone played with dumping the output of print
universes plus the constraint that is reported as inconsistent into some
external tool that finds irreducible infeasible subsets for the
underlying ILP? (Does there even exist open source software finding these?)

Best,
Christian