The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Samuel E. Moelius III wrote:
> 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.

You can get the type of an existential variable with [type of], like you 
can with any term.  Thus, it's easy to get and [assert] that type.  
However, now I'm seeing muad's point, as I can't see a way to 
instantiate the original variable with the result, since that result is 
opaque and so not valid in the existential's context.