Module `Notgram_ops`

val level_eq : Notation_gram.level -> Notation_gram.level -> bool
val entry_relative_level_eq : Constrexpr.entry_relative_level -> Constrexpr.entry_relative_level -> bool

val declare_notation_level : Constrexpr.notation -> Notation_gram.notation_grammar option -> Notation_gram.level -> unit
val level_of_notation : Constrexpr.notation -> Notation_gram.notation_grammar option * Notation_gram.level: raise Not_found if not declared

val get_defined_notations : unit -> Constrexpr.notation list: Returns notations with defined parsing/printing rules