The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

Pierre Courtieu wrote:
> Until this is implemented, let me suggest a very ugly combination of
> assert + abstract. The ugly part is that the definition name generated
> by abstract is automatically chosen by coq (it seems deterministic
> however) and that you have to look at the environment to know it. The
> other ugly part is that you have to put the abstract on the hole set
> of tactics used to prove the sub-lemma, which forces you to put
> semi-colons everywhere.

Technically, it does not work as the term produced through abstract is
opaque, so we end up with the very same problem as assert.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature