The Coq mailing list

[Taral <taralx AT gmail.com>]

On Mon, Mar 9, 2009 at 12:21 AM, Yves Bertot
<Yves.Bertot AT sophia.inria.fr>
 wrote:
> Would that fit the need?

Yes, so long as the substituted term was transparent. Much of the
difficulty comes when you have things like this:

let (p1,_) = ?12 in let (_, p2) = p1 in ...

The e* tactics can't unify this the way I want them to. What I
frequently want is to convert this to a goal of the form:

{ x : T | let (p1,_) = x in let (_, p2) = p1 in ... }

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown