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.

Thank you, it seem to do the trick!

The typical proofs of ESC/Java verification conditions can be now
checked (no proofs of the theory conflicts yet) in a few seconds.

--
  Micha³