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: 41a1251ca5ac2515d23b7acb71782182a158ff22 (plain)

1
2
3

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