coq 8.9.1 · OCaml Package

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 pr_constr_n_env : 
  Environ.env ->
  Evd.evar_map ->
  Notation_gram.tolerability ->
  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_econstr_n_env : 
  Environ.env ->
  Evd.evar_map ->
  Notation_gram.tolerability ->
  EConstr.t ->
  Pp.t

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_n_env : 
  Environ.env ->
  Evd.evar_map ->
  Notation_gram.tolerability ->
  Ltac_pretype.closed_glob_constr ->
  Pp.t

val pr_closed_glob_env : 
  Environ.env ->
  Evd.evar_map ->
  Ltac_pretype.closed_glob_constr ->
  Pp.t

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_env : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.unsafe_judgment ->
  Pp.t * Pp.t

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_decl : 
  Environ.env ->
  Evd.evar_map ->
  Constr.named_declaration ->
  Pp.t

val pr_compacted_decl : 
  Environ.env ->
  Evd.evar_map ->
  Constr.compacted_declaration ->
  Pp.t

val pr_rel_decl : Environ.env -> Evd.evar_map -> Constr.rel_declaration -> 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_evars : Evd.evar_map -> 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 =

| Constant of Names.Constant.t
| Positive of Names.MutInd.t
| Guarded of Names.Constant.t

type context_object =

| Variable of Names.Id.t
| Axiom of axiom * (Names.Label.t * Constr.rel_context * Constr.types) list
| Opaque of Names.Constant.t
| Transparent of Names.Constant.t

module ContextObjectSet : sig ... end

module ContextObjectMap : sig ... end

val pr_assumptionset : 
  Environ.env ->
  Evd.evar_map ->
  Constr.types ContextObjectMap.t ->
  Pp.t

val pr_goal_by_id : proof:Proof.t -> Names.Id.t -> Pp.t

package coq