The Coq mailing list

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

I wonder if this is an issue similar to the MacOSX one that forces
people to use the exact same version of OCaml used to build the
version of Coq that exists in the installer.

Thomas


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