The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Hi,

the subject has been discussed on this list before, and I am not aware
of any tooling advances made since then. The two treads I have been
involved in are:

https://sympa.inria.fr/sympa/arc/coq-club/2018-09/msg00008.html
https://sympa.inria.fr/sympa/arc/coq-club/2019-11/msg00087.html

I hope this helps!

Best,
Christian

On 4/10/20 1:14 AM, Yao Li wrote:
> Dear All,
> 
> I am having some recurring universe inconsistency problems lately and I 
> would like to know if there are any commands/tools for helping me debugging 
> what happened.
> 
> For example, a recurring pattern is that Coq complains to me that it cannot 
> unify two universe levels (assuming they are u1 and u4) because “u1 <= u2 < 
> u3 <= u4” or “u1 <= u2 < u3 = u4”. I would like to know where the 
> constraints concerning u3 and u4 (and perhaps other relevant constraints as 
> well) are generated—or better yet, why. However, I haven’t found a tool for 
> doing that.
> 
> I have tried “Set Printing Universes”. Unfortunately, the constraints 
> concerning u3 and u4 cannot be found at any relevant definitions. I have 
> also tried “Print Universes”, but I cannot find what I’m looking for in the 
> sea of constraints that Coq shows me.
> 
> Best,
> Yao
>