Module Notgram_ops
- val level_eq : Notation_gram.level -> Notation_gram.level -> bool
Declare and test the level of a (possibly uninterpreted) notation
- val declare_notation_level : ?onlyprint:bool -> Constrexpr.notation -> Notation_gram.level -> unit
- val level_of_notation : ?onlyprint:bool -> Constrexpr.notation -> Notation_gram.level
- raise - Not_foundif no level or not respecting onlyprint