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

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