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 -> Constr.constr -> Pp.t
val pr_lconstr : Constr.constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_lconstr_goal_style_env : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val pr_constr_env : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val pr_constr : Constr.constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_constr_goal_style_env : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val safe_pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val safe_pr_lconstr : Constr.constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val safe_pr_constr_env : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val safe_pr_constr : Constr.constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t
val pr_econstr : EConstr.t -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t
val pr_leconstr : EConstr.t -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_etype_env : Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
val pr_letype_env : Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
val pr_open_constr_env : Environ.env -> Evd.evar_map -> Evd.open_constr -> Pp.t
val pr_open_constr : Evd.open_constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_open_lconstr_env : Environ.env -> Evd.evar_map -> Evd.open_constr -> Pp.t
val pr_open_lconstr : Evd.open_constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
val pr_constr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_goal_concl_style_env : Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
val pr_ltype_env : Environ.env -> Evd.evar_map -> Constr.types -> Pp.t
val pr_ltype : Constr.types -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_type_env : Environ.env -> Evd.evar_map -> Constr.types -> Pp.t
val pr_type : Constr.types -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_lglob_constr_env : Environ.env -> 'a Glob_term.glob_constr_g -> Pp.t
val pr_lglob_constr : 'a Glob_term.glob_constr_g -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_glob_constr_env : Environ.env -> 'a Glob_term.glob_constr_g -> Pp.t
val pr_glob_constr : 'a Glob_term.glob_constr_g -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
val pr_lconstr_pattern : Pattern.constr_pattern -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
val pr_constr_pattern : Pattern.constr_pattern -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
val pr_cases_pattern : Glob_term.cases_pattern -> Pp.t
val pr_sort : Evd.evar_map -> Sorts.t -> Pp.t
val pr_polymorphic : bool -> Pp.t
val pr_cumulative : bool -> bool -> Pp.t
val pr_universe_instance : Evd.evar_map -> Univ.Instance.t -> Pp.t
val pr_universe_ctx : Evd.evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t
val pr_universe_ctx_set : Evd.evar_map -> Univ.ContextSet.t -> Pp.t
val pr_constant_universes : Evd.evar_map -> Entries.constant_universes_entry -> Pp.t
val pr_cumulativity_info : Evd.evar_map -> Univ.CumulativityInfo.t -> Pp.t
val pr_global_env : Names.Id.Set.t -> Names.GlobRef.t -> Pp.t
val pr_global : Names.GlobRef.t -> Pp.t
val pr_constant : Environ.env -> Names.Constant.t -> Pp.t
val pr_existential_key : Evd.evar_map -> Evar.t -> Pp.t
val pr_existential : Environ.env -> Evd.evar_map -> Constr.existential -> Pp.t
val pr_constructor : Environ.env -> Names.constructor -> Pp.t
val pr_inductive : Environ.env -> Names.inductive -> Pp.t
val pr_evaluable_reference : Names.evaluable_global_reference -> Pp.t
val pr_pconstant : Environ.env -> Evd.evar_map -> Constr.pconstant -> Pp.t
val pr_pinductive : Environ.env -> Evd.evar_map -> Constr.pinductive -> Pp.t
val pr_pconstructor : Environ.env -> Evd.evar_map -> Constr.pconstructor -> Pp.t
val set_compact_context : bool -> unit
val get_compact_context : unit -> bool
val pr_context_unlimited : Environ.env -> Evd.evar_map -> Pp.t
val pr_ne_context_of : Pp.t -> Environ.env -> Evd.evar_map -> Pp.t
val pr_named_context : Environ.env -> Evd.evar_map -> Constr.named_context -> Pp.t
val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t
val pr_rel_context : Environ.env -> Evd.evar_map -> Constr.rel_context -> Pp.t
val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t
val pr_context_of : Environ.env -> Evd.evar_map -> Pp.t
val pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t
val pr_cpred : Names.Cpred.t -> Pp.t
val pr_idpred : Names.Id.Pred.t -> Pp.t
val pr_transparent_state : Names.transparent_state -> Pp.t
val pr_goal : ?diffs:bool -> ?og_s:Proof_type.goal Evd.sigma -> Proof_type.goal Evd.sigma -> Pp.t
val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(Evd.evar_map * Evar.t Evar.Map.t) -> Pp.t option -> Evd.evar_map -> seeds:Proof_type.goal list -> shelf:Proof_type.goal list -> stack:int list -> unfocused:Proof_type.goal list -> goals:Proof_type.goal list -> Pp.t
val pr_subgoal : int -> Evd.evar_map -> Proof_type.goal list -> Pp.t
val pr_concl : int -> ?diffs:bool -> ?og_s:Proof_type.goal Evd.sigma -> Evd.evar_map -> Proof_type.goal -> Pp.t
val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Proof.t -> Pp.t
val pr_open_subgoals : proof:Proof.t -> Pp.t
val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t
val pr_evar : Evd.evar_map -> (Evar.t * Evd.evar_info) -> Pp.t
val pr_evars_int : Evd.evar_map -> shelf:Proof_type.goal list -> givenup:Proof_type.goal list -> int -> Evd.evar_info Evar.Map.t -> Pp.t
val pr_ne_evar_set : Pp.t -> Pp.t -> Evd.evar_map -> Evar.Set.t -> Pp.t
val pr_prim_rule : Proof_type.prim_rule -> Pp.t
  • deprecated [pr_prim_rule] is scheduled to be removed along with the legacy proof engine
val print_and_diff : Proof.t option -> Proof.t option -> unit
val prterm : Constr.constr -> Pp.t
  • deprecated The global printing API is deprecated, please use the _env functions
type axiom =
  1. | Constant of Names.Constant.t
  2. | Positive of Names.MutInd.t
  3. | Guarded of Names.Constant.t
type context_object =
  1. | Variable of Names.Id.t
  2. | Axiom of axiom * (Names.Label.t * Constr.rel_context * Constr.types) list
  3. | Opaque of Names.Constant.t
  4. | Transparent of Names.Constant.t
module ContextObjectSet : sig ... end
module ContextObjectMap : sig ... end
val pr_goal_by_id : proof:Proof.t -> Names.Id.t -> Pp.t