package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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_glob_sort_name : Glob_term.glob_sort_name -> Pp.t
val pr_glob_level : Glob_term.glob_level -> Pp.t
val pr_glob_sort : Glob_term.glob_sort -> Pp.t
val pr_record_body : (Libnames.qualid * Constrexpr.constr_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
type term_pr = {
  1. pr_constr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
  2. pr_lconstr_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t;
  3. pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> Constrexpr.constr_pattern_expr -> Pp.t;
  4. 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
OCaml

Innovation. Community. Security.