The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Thanks!

My problem was  that in the html version of Coq.Init.Datatypes which is 
linked with standard Coq documentation there is no  Set Implicit Arguments 
command .

V.
  



On Jun 30, 2011, at 3:02 PM, Pierre Courtieu wrote:

> 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.
>>