The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thanks!

However, I seem to be getting

Camlp4: Uncaught exception: DynLoader.Error ("D:\\Program Files (x86)\\Coq/lib/parsing/grammar.cma", "interface mismatch on Array")

when I run make.

(I'm also using coq 8.4 beta2, though I need to do some manual tweaking of the makefile because coqtop -config doesn't like me.)

-Jason

On Sun, Jul 1, 2012 at 5:40 PM, Thomas Braibant <thomas.braibant AT gmail.com> wrote:

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