Ppconstr (rocq-runtime.Ppconstr)

type flags = {

parentheses : bool;

}

val current_flags : unit -> flags

val of_extern_flags : PrintingFlags.Extern.t -> flags

val of_printing_flags : PrintingFlags.t -> flags

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_quality_expr : Constrexpr.quality_expr -> Pp.t

val pr_guard_annot : 
  (Constrexpr.constr_expr -> Pp.t) ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.fixpoint_order_expr option ->
  Pp.t

val pr_record : 
  string ->
  string ->
  Pp.t option ->
  ('a -> Pp.t) ->
  'a list ->
  Pp.t

val pr_record_body : 
  string ->
  string ->
  ('a -> Pp.t) ->
  Pp.t option ->
  (Libnames.qualid * 'a) list ->
  Pp.t

val pr_binders : 
  flags:flags ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.local_binder_expr list ->
  Pp.t

val pr_constr_pattern_expr : 
  flags:flags ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_pattern_expr ->
  Pp.t

val pr_lconstr_pattern_expr : 
  flags:flags ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_pattern_expr ->
  Pp.t

val pr_constr_expr : 
  flags:flags ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Pp.t

val pr_lconstr_expr : 
  flags:flags ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Pp.t

val pr_cases_pattern_expr : 
  flags:flags ->
  Constrexpr.cases_pattern_expr ->
  Pp.t

val pr_constr_expr_n : 
  flags:flags ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.entry_relative_level ->
  Constrexpr.constr_expr ->
  Pp.t

type term_pr = {

pr_constr_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
pr_lconstr_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
pr_constr_pattern_expr : flags:flags -> Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t;
pr_lconstr_pattern_expr : flags:flags -> 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 : flags:flags -> Constrexpr.constr_expr -> Pp.t

val pr_top : flags:flags -> Constrexpr.constr_expr -> Pp.t

val modular_constr_pr : 
  flags:flags ->
  ((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

module CompactedDecl : sig ... end

val compact_named_context : 
  Evd.evar_map ->
  Environ.named_context_val ->
  CompactedDecl.t list