Ppconstr
This module implements pretty-printers for constr_expr syntactic objects and their subcomponents.
The default pretty-printers produce pretty-printing commands (Pp.t
).
val prec_less :
Constrexpr.entry_level ->
Constrexpr.entry_relative_level ->
bool
val pr_tight_coma : unit -> 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_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 modular_constr_pr :
( ( unit -> Pp.t ) ->
Constrexpr.entry_relative_level ->
Constrexpr.constr_expr ->
Pp.t ) ->
( unit -> Pp.t ) ->
Constrexpr.entry_relative_level ->
Constrexpr.constr_expr ->
Pp.t