package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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_safe_judgment : Environ.env -> Evd.evar_map -> Safe_typing.judgment -> Pp.std_ppcmds
val print_opaque_name : Libnames.reference -> 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 = {
  1. print_inductive : Names.mutual_inductive -> Pp.std_ppcmds;
  2. print_constant_with_infos : Names.constant -> Pp.std_ppcmds;
  3. print_section_variable : Names.variable -> Pp.std_ppcmds;
  4. print_syntactic_def : Names.kernel_name -> Pp.std_ppcmds;
  5. print_module : bool -> Names.module_path -> Pp.std_ppcmds;
  6. print_modtype : Names.module_path -> Pp.std_ppcmds;
  7. print_named_decl : Context.Named.Declaration.t -> Pp.std_ppcmds;
  8. print_library_entry : bool -> (Libnames.object_name * Lib.node) -> Pp.std_ppcmds option;
  9. print_context : bool -> int option -> Lib.library_segment -> Pp.std_ppcmds;
  10. print_typed_value_in_env : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.types) -> Pp.std_ppcmds;
  11. 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
OCaml

Innovation. Community. Security.