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

summary refs log tree commit diff

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

blob: 6f2bcb9685f1bc9dc61a38e7ccf0b2d375dc15c4 (plain)

1
2
3

Check match 2 with 0 => 0 | S n => n end.
Notation "|" := 1 (compat "8.6").
Check match 2 with 0 => 0 | S n => n end. (* fails *)