The Coq mailing list

[andr� hirschowitz <ah AT unice.fr>]

In fact I doubt that assert is what andre wishes, as I think andre wanted to say,
 "assert (H: P)." produces an opaque term, and sometimes (it happened to me), we
 should want a transparent term with usable definition.

Exactly. I just want to give a name to an awful term which I am unable to write although I am able to produce it in proof mode.

That makes me think of a maybe real solution, but I am not sure it works:
instead of a "pose (H := _ : P).", you should try a "Lemma H: P."

No, this does not work because the local environment is not taken into account by this command (if my experiment is correct). Neither does Definition for the same reason.

Thanks to all.

ah