The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

I hacked a quick plugin that seems to do what you want in a crude way.

It provides several new vernacular commands that:
- make it possible to file the current universe constraints (giving it a 
name);
- compute the difference between two sets universe constraints that
were filed before  (using two names);
- compute the  difference between the current universe constraints and
a set of universe constraints that were filed before.

Hope that helps.
Thomas

PS: The name of the vernacular command may sound weird, but I could
not use something starting with "Save".

On Sun, Jul 1, 2012 at 4:47 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> 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

Attachment: jason.tar
Description: Unix tar archive