The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

Hi,

I often want to use the [assert] tactic:

assert (x : T)

    [proof of T]

[other proof using T]

The problem is that after T has been proven, the proof is hidden: the new element in the context is [x : T] and I cannot use the structure of the proof of T I have given (and if I wanted to construct a dependent pair whose first element is [x], I can’t).

How can I have [x := [proof term I just constructed] : T] in the context instead?

(note that I want to construct x using tactics, I do not want to write the term explicitely).

Thanks!

Guillaume