Ppextend (u.75d6a066538fb738038ab1b402df0edb.coq.8.14.1.doc.coq-core.parsing.Ppextend)

Pretty-print.

Sourcetype ppbox =

| PpHB
| PpHOVB of int
| PpHVB of int
| PpVB of int

Sourcetype ppcut =

| PpBrk of int * int
| PpFnl

Sourceval ppcmd_of_box : ppbox -> Pp.t -> Pp.t

Sourceval ppcmd_of_cut : ppcut -> Pp.t

Printing rules for notations

Sourcetype pattern_quote_style =

| QuotedPattern
| NotQuotedPattern

Sourcetype unparsing =

| UnpMetaVar of Constrexpr.entry_relative_level * Extend.side option
| UnpBinderMetaVar of Constrexpr.entry_relative_level * pattern_quote_style
| UnpListMetaVar of Constrexpr.entry_relative_level * unparsing list * Extend.side option
| UnpBinderListMetaVar of 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

Sourcetype unparsing_rule = unparsing list * Constrexpr.entry_level

Sourcetype extra_unparsing_rules = (string * string) list

Sourceval unparsing_eq : unparsing -> unparsing -> bool

Source

val declare_generic_notation_printing_rules : 
  Constrexpr.notation ->
  reserved:bool ->
  extra:extra_unparsing_rules ->
  unparsing_rule ->
  unit

Source

val declare_specific_notation_printing_rules : 
  Constrexpr.specific_notation ->
  extra:extra_unparsing_rules ->
  unparsing_rule ->
  unit

Sourceval has_generic_notation_printing_rule : Constrexpr.notation -> bool

Source

val find_generic_notation_printing_rule : 
  Constrexpr.notation ->
  unparsing_rule * bool * extra_unparsing_rules

Source

val find_specific_notation_printing_rule : 
  Constrexpr.specific_notation ->
  unparsing_rule * extra_unparsing_rules

Source

val find_notation_printing_rule : 
  Constrexpr.notation_with_optional_scope option ->
  Constrexpr.notation ->
  unparsing_rule

Source

val find_notation_extra_printing_rules : 
  Constrexpr.notation_with_optional_scope option ->
  Constrexpr.notation ->
  extra_unparsing_rules

Source

val add_notation_extra_printing_rule : 
  Constrexpr.notation ->
  string ->
  string ->
  unit