The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

I may very well have misunderstood your question but isn't Set Implicit Arguments what you are looking for?

Set Implicit Arguments.

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

Print foo_id.
(*
foo_id =
fun (A : Type) (a : A) => a
     : forall A : Type, A -> A

Argument A is implicit
Argument scopes are [type_scope _]
*)

A is implicit but not maximally inserted.

Théo

Le mar. 13 déc. 2016 à 10:58, Ralf Jung <jung AT mpi-sws.org> a écrit :

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