The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Does someone have an explanation and a work around for this behaviour?

Certainly.

First Cedric's guess is, to the best of my knowledge, inaccurate. The [eauto] tactics only knows about one single goal when it starts, and [t;eauto] will apply [eauto] sequentially on each of the goals generated by [t] (from the first to the last).

As it happens, in v8.4 and earlier releases, a semantically dubious choice was made about existential variable for efficiency reasons: the information about existential variable instantiation is propagate only at the end of a phrase (that is any change to the state of existential variables effected by a tactic will not be visible until after the period). The development version of Coq (and the next release) do not share this behaviour. So the call to [eauto] on the second goal does not see the instantiation performed by the call on the first goal.

In the meantime, the [instantiate] tactic (without argument) is a way to manually ask the system to propagate the existential variable information. And writing [eapply H_Consequence_pre;(eauto;instantiate)] should ensure that the instantiations are propagated after each successful [eauto] application and solve your problem.