3753.v « opened « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/opened/3753.v

blob: 05d77c831bae3a7b28d77fd9aff9af649231c9f8 (plain)

Axiom foo : Type -> Type.
Axiom bar : forall (T : Type), T -> foo T.
Arguments bar A x : rename.
Fail About bar.