The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

muad wrote:
> > You can do it with an Ltac function that uses [type of] and [assert] 
>
> This is almost good enough, we just don't have a way (as far as I am aware)
> of asserting (or cutting) such that the term you produce is not opaque in
> the original context.

Could someone be a little more specific, e.g., what would a call to this 
Ltac function look like?

It is not clear to me how you could get the type of an existential variable 
in Ltac.

Thank you everyone for your help, BTW.  :)

Sam