Library Coqdoc.bug11353

Definition a := 0. #[ universes( template) ]
Inductive mysum (A B:Type) : Type :=
  | myinl : A → mysum A B
  | myinr : B → mysum A B.

#[local]Definition b := 1.