The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

The message is due to the use of the [intro] tactic which is done when the goal is created. You could do something a bit more verbose like:

 Definition nat_compose : forall
     (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.

Proof.

  intros F ? G ? H ? f g.

It should work. I may be able to arrange that the trunk would have a less surprising behaviour if that is considered better.

On 4 August 2014 17:40, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

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