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

1
2
3

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