The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Do you have a test case?  I tried a few simple cases, and couldn't 
replicate the behavior.  Such as:

Variables P Q R : Type.

Definition foo{p : P}(q : Q) : R.
Admitted.

Axiom bar : P -> Q.

Axiom p : P.

Goal R.
eapply foo; apply bar. (*no error, implicit P goal of foo is shelved*)
apply p.
Unshelve.
apply p.
Qed.

-- Jonathan



On 06/19/2015 11:47 AM, Armaël Guéneau wrote:
> 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