The Coq mailing list

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

On 06/19/2015 07:49 PM, Jonathan Leivent wrote:
> Do you have a test case?  I tried a few simple cases, and couldn't replicate the behavior.

Sure. Actually, I didn't have a simple one at first; now I have
something.  Minimizing the thing was not as simple as I expected, as I
couldn't understand clearly when some subgoal was going to be shelved.

The behavior I observed seems to appear on implicit parameters
specified using Context in a section. So, anyway, here's a test case
(maybe not minimal).

    Definition filter (A: Type) := (A -> Prop) -> Prop.

    Class Filter {A: Type} (f: filter A) := {
      filter_foo : False
    }.

    Section S.
      Context {A: Type} {f: filter A} `{@Filter A f}.
 
      Lemma filter_universe:
        forall P : A -> Prop,
        (forall a, P a) ->
        f P.
      Proof. admit. Admitted.
    End S.

    Axiom f : filter unit.
    Axiom P : Prop.
    Axiom p : P.

    Goal f (fun _ => P).
      (* Succeeds. *)
      eapply filter_universe; intros. apply p.
      (* Fails. *)
      eapply filter_universe; intros; apply p.


(Of course here, the goal is not solved by the first line, but the
application of tactics succeeds, leaving a shelved goal to be proved;
using the second line instead of the first fails.)