The Coq mailing list

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

Hello world,

How can I pose a local definition within a proof

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 
?

Thanks for your attention.

ah