bug_11360.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/closed/bug_11360.v

blob: d8bc4a9f021039c3589173aeee40cfd6a52120be (plain)

Section S.
  Variable (A:Type).
  #[universes(template)]
  Inductive bar (d:A) := .
End S.
Check bar nat 0.