Module Ppextend

Pretty-print.
type ppbox =
| PpHB of int
| PpHOVB of int
| PpHVB of int
| PpVB of int
type ppcut =
| PpBrk of int * int
| PpFnl
val ppcmd_of_box : ppbox -> Pp.t -> Pp.t
val ppcmd_of_cut : ppcut -> Pp.t
Printing rules for notations
type unparsing =
| UnpMetaVar of int * Notation_gram.parenRelation
| UnpBinderMetaVar of int * Notation_gram.parenRelation
| UnpListMetaVar of int * Notation_gram.parenRelation * unparsing list
| UnpBinderListMetaVar of int * bool * unparsing list
| UnpTerminal of string
| UnpBox of ppbox * unparsing Loc.located list
| UnpCut of ppcut

Declare and look for the printing rule for symbolic notations

type unparsing_rule = unparsing list * Notation_gram.precedence
type extra_unparsing_rules = (string * string) list
val declare_notation_rule : Constrexpr.notation -> extra:extra_unparsing_rules -> unparsing_rule -> Notation_gram.notation_grammar -> unit
val find_notation_printing_rule : Constrexpr.notation -> unparsing_rule
val find_notation_extra_printing_rules : Constrexpr.notation -> extra_unparsing_rules
val find_notation_parsing_rules : Constrexpr.notation -> Notation_gram.notation_grammar
val add_notation_extra_printing_rule : Constrexpr.notation -> string -> string -> unit
val get_defined_notations : unit -> Constrexpr.notation list

Returns notations with defined parsing/printing rules