The Coq mailing list

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

Hi all,

is there a syntax to make an argument of a Definition *minimally*
inserted?  I know the following syntax:

  Definition foo_id {A : Type} (a : A) := a.

However, this makes A *maximally* inserted.  Of course I can then use
Arguments to make it minimally inserted, but (a) this has the potential
of de-syncing with the definition and (b) the place where I need this is
a section variable where I would have to re-declare Arguments for each
definition inside the section. That's not a scalable option.

What I am looking for is either an option ("Set ...") to configure
whether the curly braces make arguments minimally or maximally implicit,
or another syntax (an alternative to the curly braces) that makes them
minimally implicit.  Does something like that exist?

I found "Unset Maximal Implicit Insertion.", but that affects only the
arguments that are automatically made implicit, not those that are
declared implicit by using curly braces.

Kind regards,
Ralf