The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Yes, it’s unfortunate, at least they’d have to be marked somehow so that
when we simplify [x = y] (x and y being variables) we can substitute
the fresh one by the user-provided one. And then there might be more
intricate cases due to unification, it's doable though, as dependent 
pattern-matching in general can do that.

Best,
— Matthieu

On 28 déc. 2013, at 18:15, Ian Lynagh 
<igloo AT earth.li>
 wrote:

> On Fri, Dec 27, 2013 at 01:46:56PM +0000, Ian Lynagh wrote:
>> 
>> Aha, thanks! In this case it looks like
>>    generalize_eqs H ;
>>    introduce H ;
>>    destruct H as [X | Y] ;
>>    simpl_dep_elim.
>> works
> 
> Ah, having fiddled with this further, it looks like at least some of the
> variables that I care about are actually coming from 'fresh' calls in
> simplify_one_dep_elim_term (i.e. part of the simpl_dep_elim call). So
> life isn't as simple as I'd hoped  :-(
> 
> 
> Thanks
> Ian
>