coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Printing new universes

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Printing new universes
Date: Sun, 1 Jul 2012 16:47:40 -0400

Hi,

Is there a way to ask coq for the new universe constraints that were introduced by a particular definition or theorem? Alternatively, is there a way to script emacs, running Proof General, to save the output of [Print Universes] at one point, and diff that against the output of [Print Universes] at another point, and show some number of surrounding lines?

Thanks.

-Jason

[Coq-Club] Printing new universes, Jason Gross, 07/01/2012
- Re: [Coq-Club] Printing new universes, Thomas Braibant, 07/01/2012
  - Re: [Coq-Club] Printing new universes, Thomas Braibant, 07/01/2012
    - Re: [Coq-Club] Printing new universes, Jason Gross, 07/02/2012
      - Re: [Coq-Club] Printing new universes, Thomas Braibant, 07/02/2012