The Coq mailing list

[Carlos.SIMPSON AT unice.fr]

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.
---Carlos Simpson