The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi, Paolo --

You can't modify the section context from within a tactic, but you can general a variable of a particular type. Just use the [cut] tactic:

n : nat 

===================

n + 0 = n

cut nat.

will produce two goals:

n : nat

===================

nat -> n + 0 = nat

n : nat

===================

nat

Cutting something like [nat] is a little bit strange though, usually you cut things in Prop.

Hope this helps.

On Sat, Jun 2, 2012 at 8:37 AM, Paolo Herms <paolo.herms AT inria.fr> wrote:

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

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/