coq 8.7.2 · OCaml Package

val assumptions_for_print : Names.Name.t list -> Termops.names_context

val print_closed_sections : bool Pervasives.ref

val print_context : bool -> int option -> Lib.library_segment -> Pp.std_ppcmds

val print_library_entry : 
  bool ->
  (Libnames.object_name * Lib.node) ->
  Pp.std_ppcmds option

val print_full_context : unit -> Pp.std_ppcmds

val print_full_context_typ : unit -> Pp.std_ppcmds

val print_full_pure_context : unit -> Pp.std_ppcmds

val print_sec_context : Libnames.reference -> Pp.std_ppcmds

val print_sec_context_typ : Libnames.reference -> Pp.std_ppcmds

val print_judgment : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.unsafe_judgment ->
  Pp.std_ppcmds

val print_safe_judgment : 
  Environ.env ->
  Evd.evar_map ->
  Safe_typing.judgment ->
  Pp.std_ppcmds

val print_eval : 
  Reductionops.reduction_function ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  EConstr.unsafe_judgment ->
  Pp.std_ppcmds

val print_name : Libnames.reference Misctypes.or_by_notation -> Pp.std_ppcmds

val print_opaque_name : Libnames.reference -> Pp.std_ppcmds

val print_about : Libnames.reference Misctypes.or_by_notation -> Pp.std_ppcmds

val print_impargs : 
  Libnames.reference Misctypes.or_by_notation ->
  Pp.std_ppcmds

val print_graph : unit -> Pp.std_ppcmds

val print_classes : unit -> Pp.std_ppcmds

val print_coercions : unit -> Pp.std_ppcmds

val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.std_ppcmds

val print_canonical_projections : unit -> Pp.std_ppcmds

val print_typeclasses : unit -> Pp.std_ppcmds

val print_instances : Globnames.global_reference -> Pp.std_ppcmds

val print_all_instances : unit -> Pp.std_ppcmds

val inspect : int -> Pp.std_ppcmds

val print_located_qualid : Libnames.reference -> Pp.std_ppcmds

val print_located_term : Libnames.reference -> Pp.std_ppcmds

val print_located_tactic : Libnames.reference -> Pp.std_ppcmds

val print_located_module : Libnames.reference -> Pp.std_ppcmds

type object_pr = {

print_inductive : Names.mutual_inductive -> Pp.std_ppcmds;
print_constant_with_infos : Names.constant -> Pp.std_ppcmds;
print_section_variable : Names.variable -> Pp.std_ppcmds;
print_syntactic_def : Names.kernel_name -> Pp.std_ppcmds;
print_module : bool -> Names.module_path -> Pp.std_ppcmds;
print_modtype : Names.module_path -> Pp.std_ppcmds;
print_named_decl : Context.Named.Declaration.t -> Pp.std_ppcmds;
print_library_entry : bool -> (Libnames.object_name * Lib.node) -> Pp.std_ppcmds option;
print_context : bool -> int option -> Lib.library_segment -> Pp.std_ppcmds;
print_typed_value_in_env : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.types) -> Pp.std_ppcmds;
print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.std_ppcmds;

}

val set_object_pr : object_pr -> unit

val default_object_pr : object_pr

package coq