Module Ppconstr

This module implements pretty-printers for constr_expr syntactic objects and their subcomponents.

val pr_tight_coma : unit -> Pp.t
val pr_with_comments : ?⁠loc:Loc.t -> Pp.t -> Pp.t
val pr_com_at : int -> Pp.t
val pr_sep_com : (unit -> Pp.t) -> (Constrexpr.constr_expr -> Pp.t) -> Constrexpr.constr_expr -> Pp.t
val pr_id : Names.Id.t -> Pp.t
val pr_qualid : Libnames.qualid -> Pp.t
val pr_patvar : Pattern.patvar -> Pp.t
val pr_sort_name_expr : Constrexpr.sort_name_expr -> Pp.t
val pr_univ_level_expr : Constrexpr.univ_level_expr -> Pp.t
val pr_sort_expr : Constrexpr.sort_expr -> Pp.t
val pr_guard_annot : (Constrexpr.constr_expr -> Pp.t) -> Constrexpr.local_binder_expr list -> Constrexpr.recursion_order_expr option -> Pp.t
val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t
val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t
val pr_binders : Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> Pp.t
val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t
val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t
val pr_constr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t
val pr_lconstr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t
val pr_cases_pattern_expr : Constrexpr.cases_pattern_expr -> Pp.t
val pr_constr_expr_n : Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Constrexpr.constr_expr -> Pp.t
type term_pr = {
pr_constr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
pr_lconstr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t;
pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t;
}
val set_term_pr : term_pr -> unit
val default_term_pr : term_pr
val lsimpleconstr : Constrexpr.entry_relative_level
val ltop : Constrexpr.entry_relative_level
val pr_simpleconstr : Constrexpr.constr_expr -> Pp.t
val pr_top : Constrexpr.constr_expr -> Pp.t
val modular_constr_pr : ((unit -> Pp.t) -> int option -> Constrexpr.entry_relative_level -> Constrexpr.constr_expr -> Pp.t) -> (unit -> Pp.t) -> int option -> Constrexpr.entry_relative_level -> Constrexpr.constr_expr -> Pp.t