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

summary refs log tree commit diff

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

blob: 8b032db5f5c7bd373cdb77e316aada99a5cfaf16 (plain)

1	`Fail Notation "'forall' x .. y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder).`