(** {2 Notation enabling/disabling}
* Right now, only disabling of notation during pretty printing is supporting.
* If it is useful to disable it also for the input phase is still to be
(** {2 Notation enabling/disabling}
* Right now, only disabling of notation during pretty printing is supporting.
* If it is useful to disable it also for the input phase is still to be