The Coq mailing list

[Armaël Guéneau <armael.gueneau AT ens-lyon.fr>]

Hi,

I'm encountering a strange behavior that I can't really explain to
myself, and that seems to boil down to the interaction between the
tactic sequence (";") and tactics producing shelved goals like
eauto/eapply.

I have a Ltac tactic of the form:

Ltac tac :=
  eapply foo;
  apply bar.

(n.b.: [eapply foo] produces only one goal)

In some context, tac was failing for an unknown reason, so I inlined
it and started investigating. In this proof context, [foo] needs an
implicit argument that cannot be found directly in the context, so
eapply decides to produce the corresponding goal as a shelved goal.

So, in this context, just using [eapply foo.] succeeds, and produces a
shelved goal [H: P]. After that, I can use [apply bar.] successfully.

However, in the same proof context, [eapply foo; apply bar.] fails.
The error message is "Unable to satisfy the following constraints:
?H: P" (so, the same goal that was previously shelved).


Soooo, I don't really understand why this happens. Do you know how I
should write my [tac] tactic for it to work just as a
[eapply foo. apply bar.]?

(oh, and I'm running Coq 8.5beta2)

-- Armaël