The Coq mailing list

[St�phane Glondu <steph AT glondu.net>]

Le 20/12/2011 04:30, Kenneth Roe a écrit :
> If instead of executing three separate commands, I combine them as follows:
> 
>     *(eapply simplifyPre; [simplifyState|simpl]).*

Try instead:

 (eapply simplifyPre; [simplifyState|instantiate; simpl])

I'm not sure it will work in your case, but I suspect that it is
"simplifyState" that makes the "AbsExists" appear, but simpl cannot see
it because changes in existential variables (aka "evars", the ones
starting with ?) are not propagated everywhere in a composite tactic. It
works when executing simpl by itself because "." forces evar propagation.


Cheers,

-- 
Stéphane