bug_4690.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: f50866a990769220276559dd9e6edd7208438370 (plain)

1
2
3

(* Check that @f is not allowed in notation when f is a notation variable *)

Fail Notation "# g" := (@g O) (at level 0).