The Coq mailing list

["John Wiegley" <jwiegley AT gmail.com>]

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 global imports:

  Require Export Coq.Classes.Equivalence.
  Require Export Coq.Classes.Morphisms.
  Require Export Coq.Classes.RelationClasses.
  Require Export Coq.Setoids.Setoid.
  Require Export Coq.Unicode.Utf8.
  Require        Setoid.
  Require Export CpdtTactics.
  
  Open Scope type_scope.

Thank you,
  John