package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val print_goal_tag_opt_name : string list
val pr_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Constr.constr -> Pp.t
val safe_pr_constr_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 pr_econstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t
val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t
val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t
val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
val pr_open_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Evd.open_constr -> Pp.t
val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Evd.open_constr -> Pp.t
val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> Constr.types -> Pp.t
val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> Constr.types -> Pp.t
val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Ltac_pretype.closed_glob_constr -> Pp.t
val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
val pr_lglob_constr_env : Environ.env -> Evd.evar_map -> 'a Glob_term.glob_constr_g -> Pp.t
val pr_glob_constr_env : Environ.env -> Evd.evar_map -> 'a Glob_term.glob_constr_g -> Pp.t
val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
val pr_cases_pattern : Glob_term.cases_pattern -> Pp.t
val pr_sort : Evd.evar_map -> Sorts.t -> Pp.t
val pr_universe_instance : Evd.evar_map -> Univ.Instance.t -> Pp.t
val pr_universe_instance_constraints : Evd.evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
val pr_universe_ctx : Evd.evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t
val pr_abstract_universe_ctx : Evd.evar_map -> ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t -> Univ.AUContext.t -> Pp.t
val pr_universe_ctx_set : Evd.evar_map -> Univ.ContextSet.t -> Pp.t
val pr_universes : Evd.evar_map -> ?variance:Univ.Variance.t array -> ?priv:Univ.ContextSet.t -> Declarations.universes -> Pp.t
val universe_binders_with_opt_names : Univ.AUContext.t -> UnivNames.univ_name_list option -> UnivNames.universe_binders
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 : TransparentState.t -> Pp.t
val pr_goal : ?diffs:bool -> ?og_s:Goal.goal Evd.sigma -> Goal.goal Evd.sigma -> Pp.t
val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(Evd.evar_map * Goal.goal Evar.Map.t) -> Pp.t option -> Evd.evar_map -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t
val pr_subgoal : int -> Evd.evar_map -> Goal.goal list -> Pp.t
val pr_concl : int -> ?diffs:bool -> ?og_s:Goal.goal Evd.sigma -> Evd.evar_map -> Goal.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:Goal.goal list -> given_up:Goal.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 print_and_diff : Proof.t option -> Proof.t option -> unit
val print_dependent_evars : Evar.t option -> Evd.evar_map -> Evar.t list -> Pp.t
type axiom =
  1. | Constant of Names.Constant.t
  2. | Positive of Names.MutInd.t
  3. | Guarded of Names.GlobRef.t
  4. | TypeInType of Names.GlobRef.t
  5. | UIP of Names.MutInd.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
val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
val pr_typing_flags : Declarations.typing_flags -> Pp.t
val print_goal_names : unit -> bool