The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

Does the Qed say why it fails?
I am under the impression that universe constraints are not the only
term building constraints.

Kind regards, Jonas

2012/2/24 Gregory Malecha 
<gmalecha AT eecs.harvard.edu>:
> Hello,
>
> Is it possible for [Qed] to generate additional universe constraints? I'm
> working on a proof like this:
>
> Theorem ...
> Proof.
>   tactic.
>
>   Set Printing Universes.
>   Print Universes "universes".
> Qed.
>
> The final [Qed] fails, but when I look at the dump of the constraints in the
> universes file (the file can be found
> at: http://www.people.fas.harvard.edu/~gmalecha/universes), there is nothing
> inconsistent about them (I checked this using the yices smt solver). If it
> is possible for [Qed] to generate new constraints, is there any way to get
> the constraint set after it generates them so that I can find the cycle?
> (I'm experiencing this issue in 8.3pl2)
>
> Thank you.
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/
>