The Coq mailing list

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

Thanks for your answers. I’ll try to use Daniel’s first suggestion until Coq supports transparent asserts.

Guillaume

2011/9/12 Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>

This kind of tactics is beyond the capabilities of the implementation of proof&tactics of Coq 8.3. The version that is currently in trunk can handle it, but there is still quite a bit of work to do to have them (technicalities about a mismatch between user-level tactical and new tactics). It has been decided that we won't have this feature in the 8.4 release. But expectingly, they will be available in the following one.


Arnaud Spiwack

On 10 September 2011 17:20, Guillaume Brunerie <guillaume.brunerie AT gmail.com> wrote:

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