The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi Hugo,

> I just replied to your bug report. I'm afraid the misunderstanding
> comes from the maximal implicit argument of foo.
> 
> Indeed, if you type
> 
>   Set Printing Existential Instances.
> 
> and do
> 
>   Check foo.
>   (*
>   foo
>        : forall P0 Q0 : Prop, ?n@{P:=P; Q:=Q; H:=H; H0:=H0} = 0 -> Q0 -> P0 
> -> Q0
>   *)
> 
> You'll see that the type of foo depends on the "P" of the goal and
> that there is no other choice than renaming the "P" of foo into
> another name.

I do not understand this syntax. What is the "?n@{...}"?
Also, what you say does not seem to explain why this only happens when
[foo] was declared in a Section.

However, disregarding the details of the implementation, don't you agree
that having to write

  foo (P0:=P)

when foo was actually declared as having type "forall P:Prop, ..." is
very confusing? There is no ambiguity here, I am writing an application
of [foo] which only has one parameter called [P].
  From a user perspective, Coq is essentially making up a new name here
for something that I already named differently.

> So, probably, you intended to do
> 
>   apply @foo with (P:=P).
> 
> Hope it helps,

Being able to work around this with the @ is certainly useful. However,
since only *implicit* arguments can be named, this trick becomes
impractical once any non-implicit argument has to be specified -- it
cannot be named, so one has to resort to underscores again.

Kind regards,
Ralf