The Coq mailing list

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

On 03/08/2014 22:04, John Wiegley wrote:
> I was trying to define composition of natural transformations
>
>    Definition nat_compose
>      (F : C -> D) `{Functor F}
>      (G : C -> D) `{Functor G}
>      (H : C -> D) `{Functor H}
>      (f : Natural G H) (g : Natural F G) : Natural F H.
>
> But Coq says:
>
>    Error: H is already used.
>
> If I change H to I, everything works fine.  Since I was unable to Print H, or
> find H defined in any of my modules, I wondered if this reminded anyone of
> anything?

My guess is that, by the time Coq encounters (H : C -> D), this name has 
already been claimed by one of the {Functor ...} arguments. You can 
check whether this is the case by printing nat_compose (the version with 
I instead of H). I don't think there is a workaround, except by 
explicitly naming all your arguments.

Best regards,

Guillaume