The Coq mailing list

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

On 15/09/2017 17:02, Soegtrop, Michael wrote:
> Dear Guillaume,
> 
>> Is there a use for non-maximal implicit arguments outside of legacy code? 
>> If not,
>> adding a new binder syntax is not worth it.
> 
> Except that it would make it easier to gradually move standard library code 
> towards using maximal implicit arguments.

What do you have in mind?

For example, moving from

  Set Implicit Arguments.
  Inductive sig (A:Type) (P:A -> Prop) : Type :=
    exist : forall x:A, P x -> sig P.

to

  Set Implicit Arguments.
  Inductive sig {A:Type} (P:A -> Prop) : Type :=
    exist : forall x:A, P x -> sig P.

is already gradual. You don't need to go through

  Inductive sig [A:Type] (P:A -> Prop) : Type :=
    exist : forall x:A, P x -> sig P.

Best regards,

Guillaume