The Coq mailing list

[Paolo Herms <paolo.herms AT inria.fr>]

Hello,
I'd like to declare a section variable inside a tactic and then use it but it 
does not work. The problem seems to be that the newly declared variable is 
not 
yet valid, like says the warning in the toplevel at the Variable command:

Warning: Variable x is not visible from current goals

Can anybody explain why is that? What does "not visible" exactly mean?
Any ideas how I can work around this problem? 
Manually one would just move the variable declaration before the beginning of 
the proof, but as I'm trying to do this automatically in a tactic I can't do 
this. Do you think I can insert the variable in the proof environment in any 
way?
Thanks in advance,
-- 
Paolo Herms
PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
Paris, France