The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Daniel, I think "Unshelve." is what your are looking for.

P.

2015-10-12 13:39 GMT+02:00 Daniel de Rauglaudre 
<daniel.de_rauglaudre AT inria.fr>:
> Hi,
>
> I work in a context when proofs are very relevant (hott) and I have
> a problem.
>
> When I end an assert, the type is put in the hypotheses, but not the
> proof term. For example, when I write
>     assert (p : 2 + 2 = 4) by reflexivity.
> the line
>     p : 2 + 2 = 4
> is added in the hypotheses but not the contains of p.
>
> I would like to have the proof term also, i.e.:
>   p := eq_refl 4 : 2 + 2 = 4
>
> To resolve that, for the moment, I do the proof with assert and, then,
> I type "Show Proof" to get the proof term. I copy/paste it and I put it.
>     set (p := eq_refl 4 : 2 + 4 = 4)
>
> Of course my proofs are not as simple as "eq_refl 4".
>
> Someone (thanks to him) told me to use evar:
>     evar (p : 2 + 2 = 4).
> Then I get
>     p := ?p : 2 + 2 = 4
>
> Ok. And now? how do I prove p immediately using tactics, to fill
> my "?p"?
>
> Thank you.
>
> --
> Daniel de Rauglaudre
> http://pauillac.inria.fr/~ddr/