package coq

  1. Overview
  2. Docs
package coq
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 ref
val print_context : Environ.env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t
val print_library_entry : Environ.env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option
val print_full_context : Environ.env -> Evd.evar_map -> Pp.t
val print_full_context_typ : Environ.env -> Evd.evar_map -> Pp.t
val print_full_pure_context : Environ.env -> Evd.evar_map -> Pp.t
val print_sec_context : Environ.env -> Evd.evar_map -> Libnames.qualid -> Pp.t
val print_sec_context_typ : Environ.env -> Evd.evar_map -> Libnames.qualid -> Pp.t
val print_safe_judgment : Environ.env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
val print_opaque_name : Environ.env -> Evd.evar_map -> Libnames.qualid -> Pp.t
val print_graph : unit -> Pp.t
val print_classes : unit -> Pp.t
val print_coercions : unit -> Pp.t
val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
val print_canonical_projections : Environ.env -> Evd.evar_map -> Names.GlobRef.t list -> Pp.t
val print_typeclasses : unit -> Pp.t
val print_instances : Names.GlobRef.t -> Pp.t
val print_all_instances : unit -> Pp.t
val inspect : Environ.env -> Evd.evar_map -> int -> Pp.t
type !'a locatable_info = {
  1. locate : Libnames.qualid -> 'a option;
  2. locate_all : Libnames.qualid -> 'a list;
  3. shortest_qualid : 'a -> Libnames.qualid;
  4. name : 'a -> Pp.t;
  5. print : 'a -> Pp.t;
  6. about : 'a -> Pp.t;
}
val register_locatable : string -> 'a locatable_info -> unit
val print_located_qualid : Libnames.qualid -> Pp.t
val print_located_term : Libnames.qualid -> Pp.t
val print_located_module : Libnames.qualid -> Pp.t
val print_located_other : string -> Libnames.qualid -> Pp.t
type object_pr = {
  1. print_inductive : Names.MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
  2. print_constant_with_infos : Names.Constant.t -> UnivNames.univ_name_list option -> Pp.t;
  3. print_section_variable : Environ.env -> Evd.evar_map -> Names.variable -> Pp.t;
  4. print_syntactic_def : Environ.env -> Names.KerName.t -> Pp.t;
  5. print_module : bool -> Names.ModPath.t -> Pp.t;
  6. print_modtype : Names.ModPath.t -> Pp.t;
  7. print_named_decl : Environ.env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
  8. print_library_entry : Environ.env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option;
  9. print_context : Environ.env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
  10. print_typed_value_in_env : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.types) -> Pp.t;
  11. print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
}
val set_object_pr : object_pr -> unit
val default_object_pr : object_pr
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct