coq 8.11.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_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_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_constr_env : Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t

val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t

val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t

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_lconstr_env : 
  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_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_type_env : Environ.env -> Evd.evar_map -> Constr.types -> Pp.t

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

val pr_lglob_constr_env : Environ.env -> 'a Glob_term.glob_constr_g -> Pp.t

val pr_glob_constr_env : Environ.env -> '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 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 : 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_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 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 =

| Constant of Names.Constant.t
| Positive of Names.MutInd.t
| Guarded of Names.GlobRef.t
| TemplatePolymorphic of Names.MutInd.t
| TypeInType of Names.GlobRef.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

val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t

val pr_typing_flags : Declarations.typing_flags -> Pp.t

package coq