The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello Vladimir,

No, if you play the script of Datatype.v until the definnition of
identity and use [About identity] you will see that the argument is
already implicit. Actually this is probably due to the global [ Set
Implicit Arguments ] at the beginning of the same file.

Best regards,
Pierre

2011/6/30 Vladimir Voevodsky 
<vladimir AT ias.edu>:
> Hello,
>
> does anybody know where the first ( type ) argument of [ identity ] is 
> declared to be implicit ?
>
> [ identity ] itself is defined in Coq.Init.Datatypes but there the first 
> argument is explicit.
>
> Thanks!
> Vladimir.
>