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

about summary refs log tree commit diff

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

blob: 4125ea1c1b37bcc7717c8680a375b41fe6701cc4 (plain)

Inductive Foo : Type -> Type := foo A : Foo A.
Goal True.
  remember Foo.
Abort.