package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val enable_unfocused_goal_printing : bool ref
val enable_goal_tags_printing : bool ref
val enable_goal_names_printing : bool ref
val pr_lconstr_env : Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds
val pr_lconstr : Term.constr -> Pp.std_ppcmds
val pr_lconstr_goal_style_env : Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds
val pr_constr_env : Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds
val pr_constr : Term.constr -> Pp.std_ppcmds
val pr_constr_goal_style_env : Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds
val safe_pr_lconstr_env : Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds
val safe_pr_lconstr : Term.constr -> Pp.std_ppcmds
val safe_pr_constr_env : Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds
val safe_pr_constr : Term.constr -> Pp.std_ppcmds
val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.t -> Pp.std_ppcmds
val pr_econstr : EConstr.t -> Pp.std_ppcmds
val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.t -> Pp.std_ppcmds
val pr_leconstr : EConstr.t -> Pp.std_ppcmds
val pr_open_constr_env : Environ.env -> Evd.evar_map -> Evd.open_constr -> Pp.std_ppcmds
val pr_open_constr : Evd.open_constr -> Pp.std_ppcmds
val pr_open_lconstr_env : Environ.env -> Evd.evar_map -> Evd.open_constr -> Pp.std_ppcmds
val pr_open_lconstr : Evd.open_constr -> Pp.std_ppcmds
val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds
val pr_constr_under_binders : Pattern.constr_under_binders -> Pp.std_ppcmds
val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds
val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.std_ppcmds
val pr_goal_concl_style_env : Environ.env -> Evd.evar_map -> EConstr.types -> Pp.std_ppcmds
val pr_ltype_env : Environ.env -> Evd.evar_map -> Term.types -> Pp.std_ppcmds
val pr_ltype : Term.types -> Pp.std_ppcmds
val pr_type : Term.types -> Pp.std_ppcmds
val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds
val pr_lglob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds
val pr_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds
val pr_lconstr_pattern : Pattern.constr_pattern -> Pp.std_ppcmds
val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds
val pr_constr_pattern : Pattern.constr_pattern -> Pp.std_ppcmds
val pr_cases_pattern : Glob_term.cases_pattern -> Pp.std_ppcmds
val pr_polymorphic : bool -> Pp.std_ppcmds
val pr_cumulative : bool -> bool -> Pp.std_ppcmds
val pr_universe_instance : Evd.evar_map -> Univ.universe_context -> Pp.std_ppcmds
val pr_universe_ctx_set : Evd.evar_map -> Univ.ContextSet.t -> Pp.std_ppcmds
val pr_cumulativity_info : Evd.evar_map -> Univ.cumulativity_info -> Pp.std_ppcmds
val pr_constant : Environ.env -> Names.constant -> Pp.std_ppcmds
val pr_existential_key : Evd.evar_map -> Term.existential_key -> Pp.std_ppcmds
val pr_constructor : Environ.env -> Names.constructor -> Pp.std_ppcmds
val pr_inductive : Environ.env -> Names.inductive -> Pp.std_ppcmds
val pr_evaluable_reference : Names.evaluable_global_reference -> Pp.std_ppcmds
val pr_pconstant : Environ.env -> Term.pconstant -> Pp.std_ppcmds
val pr_pinductive : Environ.env -> Term.pinductive -> Pp.std_ppcmds
val pr_pconstructor : Environ.env -> Term.pconstructor -> Pp.std_ppcmds
val set_compact_context : bool -> unit
val get_compact_context : unit -> bool
val pr_context_unlimited : Environ.env -> Evd.evar_map -> Pp.std_ppcmds
val pr_ne_context_of : Pp.std_ppcmds -> Environ.env -> Evd.evar_map -> Pp.std_ppcmds
val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.std_ppcmds
val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds
val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.std_ppcmds
val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds
val pr_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds
val pr_predicate : ('a -> Pp.std_ppcmds) -> (bool * 'a list) -> Pp.std_ppcmds
val pr_cpred : Names.Cpred.t -> Pp.std_ppcmds
val pr_idpred : Names.Id.Pred.t -> Pp.std_ppcmds
val pr_transparent_state : Names.transparent_state -> Pp.std_ppcmds
val pr_subgoals : ?pr_first:bool -> Pp.std_ppcmds option -> Evd.evar_map -> Evd.evar list -> Goal.goal list -> int list -> Proof_type.goal list -> Proof_type.goal list -> Pp.std_ppcmds
val pr_subgoal : int -> Evd.evar_map -> Proof_type.goal list -> Pp.std_ppcmds
val pr_concl : int -> Evd.evar_map -> Proof_type.goal -> Pp.std_ppcmds
val pr_open_subgoals : ?proof:Proof.proof -> unit -> Pp.std_ppcmds
val pr_nth_open_subgoal : int -> Pp.std_ppcmds
val pr_evars_int : Evd.evar_map -> int -> Evd.evar_info Evar.Map.t -> Pp.std_ppcmds
val pr_prim_rule : Proof_type.prim_rule -> Pp.std_ppcmds
val prterm : Term.constr -> Pp.std_ppcmds
type axiom =
  1. | Constant of Names.constant
  2. | Positive of Names.MutInd.t
  3. | Guarded of Names.constant
type context_object =
  1. | Variable of Names.Id.t
  2. | Axiom of axiom * (Names.Label.t * Context.Rel.t * Term.types) list
  3. | Opaque of Names.constant
  4. | Transparent of Names.constant
module ContextObjectSet : sig ... end
module ContextObjectMap : sig ... end
val pr_goal_by_id : Names.Id.t -> Pp.std_ppcmds
val pr_goal_by_uid : string -> Pp.std_ppcmds
type printer_pr = {
  1. pr_subgoals : ?pr_first:bool -> Pp.std_ppcmds option -> Evd.evar_map -> Evd.evar list -> Goal.goal list -> int list -> Proof_type.goal list -> Proof_type.goal list -> Pp.std_ppcmds;
  2. pr_subgoal : int -> Evd.evar_map -> Proof_type.goal list -> Pp.std_ppcmds;
  3. pr_goal : Proof_type.goal Evd.sigma -> Pp.std_ppcmds;
}
val set_printer_pr : printer_pr -> unit
val default_printer_pr : printer_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