The Coq mailing list

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

Disclaimer: I tested this with coq 8.4 beta2, and the Makefile was
generated using coq_makefile jason.ml4 > Makefile

Thomas


On Sun, Jul 1, 2012 at 5:38 PM, Thomas Braibant
<thomas.braibant AT gmail.com>
 wrote:
> 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