The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

> writing something like
> pose (myname := ? : mytype)   
>  instead of 
> pose (myname := myformula )
> 
> in such a way that 
> -the next goal becomes mytype 
> -so that myformula can be generated in proof mode 

I think you are looking for the following?

  assert (myname : mytype).