The Coq mailing list

["Michal Moskal" <michal.moskal AT gmail.com>]

On 4/2/07, 
Carlos.SIMPSON AT unice.fr
 
<Carlos.SIMPSON AT unice.fr>
 wrote:
> This is just a guess, but looking at your file it looks  like you might
> want to try replacing the word
> ``Variable'' by the word ``Parameter'', and the word ``Let'' by the word
> ``Definition''.
> As you have written it, it turns the whole file into a local context,
> which is (if I understand correctly?) saved in a different
> way in Coq than the global context. Coq is designed to contain gigantic
> global contexts, but the local context is thought of
> as something that would fit in the ``current goal to be proven'' window
> in an interface.

As I said, it worked very well, thanks!

Now I'm trying to prove that the formula's negation normal form is
equivalent to the original formula. Coq seems to be stuck on my proof
of it -- it's an application of a few thousand symbols (the line
starting with "Definition skol :", I'll be trying to prove the
skolemizations later). After a few minutes it prints:

 Anomaly: uncaught exception Invalid_argument "String.create". Please report.

It might be the case (just a wild guess) that coq is trying to tell me
about an error it detected, but it doesn't like the size of the term.

I might try to break it into smaller pieces if that would help (using
intemediate definitions).

The proof is at:
 http://nemerle.org/~malekith/temp/proof.v.gz

Any ideas?

Thanks!
 Michal