make_notation.v « prerequisite « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/prerequisite/make_notation.v

blob: 4a75713d1cb608975219965450f11e4a25066cbc (plain)

1
2
3

(* Used in Notation.v to test import of notations from files in sections *)

Notation "'Z'" := O (at level 9).