The Coq mailing list

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

On 06/23/2015 05:20 PM, Jonathan Leivent wrote:
>  > This is indeed quite strange.  I tried inserting an "instantiate" in 
> that failing sequence, but that didn't help.  Also, if the failing > 
sequence is modified to be "eapply filter_universe; [|intros; apply > 
p]", it fails saying that it expects just 1 tactic (meaning it has > 
just one subgoal) - so, the failure is not due to "apply p" being > 
applied to two subgoals.  I also printed out the goal using a > 
debugging tactic just prior to the final failing "apply p", and it > is 
"a : unit |- P" just as expected. > > Furthermore, replacing that final 
"apply p" with "exact p", "eapply > p" or "refine p" makes the sequence 
work.  It also works to first > pose p, then use "assumption" in place 
of that final "apply p". > > Also, adding "Axiom g : Filter f" to the 
list of axioms makes the > final "apply p" work - evidently because then 
the "eapply > filter_universe" doesn't need to shelve the typeclass 
constriant "|- > Filter f". > > I think this is probably a bug about 
something specific to apply > vs. typeclass constraints.  It is as if 
apply alone among the > tactics believes it must solve typeclass 
constraints shelved earlier > in the sequence. >

Thanks for the investigation! I guess I should report the bug, then...

Thanks!