The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 15/09/2017 15:12, Maxime Dénès wrote:
> Hello Michael,
> 
> An idea could be to also provide the [A : Type] syntax in binders for
> non-maximal implicits, similar to what Arguments accepts.

Is there a use for non-maximal implicit arguments outside of legacy
code? If not, adding a new binder syntax is not worth it.

Best regards,

Guillaume