5205.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: 406f37a4b14f7517914c399efeec52e4e6efad57 (plain)

Definition foo (n : nat) (m : nat) : nat := m.

Arguments foo {_} _, _ _.

Check foo 1 1.
Check foo (n:=1) 1.