The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

On Wed, May 4, 2016 at 9:45 AM, Ralf Jung <jung AT mpi-sws.org> wrote:

Hi all,

[...]
These circumstances depend on whether [foo] was using variables of an
enclosing section (the [n] above), and on the current context at the
time of *applying* [foo] (the first argument of [bar] is also called
[P]). To me this was obviously a bug; I cannot imagine any situation in
which you'd *want* this behavior. Guillaume however noticed that there's
actually code in Coq doing this "on purpose".

WAT? BTW, I run into this bug, but I didn't know exactly when it happened. Good to know.

 

[...]
And while I am on it -- what is the reason that this syntax can be used
only for implicit arguments? I think it would be just as useful for
explicit arguments; for example to give arguments in a different order,
or when applying a lemma, as in [apply (lemma (arg:=foo))], without
having to specify [arg] as implicit.

+1!

 

Kind regards,
Ralf