The Coq mailing list

[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/