package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ppbox =
  1. | PpHB of int
  2. | PpHOVB of int
  3. | PpHVB of int
  4. | PpVB of int
type ppcut =
  1. | PpBrk of int * int
  2. | PpFnl
val ppcmd_of_box : ppbox -> Pp.t -> Pp.t
val ppcmd_of_cut : ppcut -> Pp.t
type unparsing =
  1. | UnpMetaVar of int * Notation_gram.parenRelation
  2. | UnpBinderMetaVar of int * Notation_gram.parenRelation
  3. | UnpListMetaVar of int * Notation_gram.parenRelation * unparsing list
  4. | UnpBinderListMetaVar of int * bool * unparsing list
  5. | UnpTerminal of string
  6. | UnpBox of ppbox * unparsing Loc.located list
  7. | UnpCut of ppcut
type unparsing_rule = unparsing list * Notation_gram.precedence
type extra_unparsing_rules = (string * string) list
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