Module Printer

These are the entry points for printing terms, context, tac, ...

val enable_unfocused_goal_printing : bool Stdlib.ref
val enable_goal_tags_printing : bool Stdlib.ref
val enable_goal_names_printing : bool Stdlib.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

Display compact contexts of goals (simple hyps on the same line)

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

pr_goal ~diffs ~og_s g_s prints the goal specified by g_s. If diffs is true, highlight the differences between the old goal, og_s, and g_s. g_s and og_s are records containing the goal and sigma for, respectively, the new and old proof steps, e.g. { it = g ; sigma = sigma }.

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

pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals prints the goals in goals followed by the goals in unfocused in a compact form (typically only the conclusion). If pr_first is true, print the first goal in full. close_cmd is printed afterwards verbatim.

If diffs is true, then highlight diffs relative to os_map in the output for first goal. os_map contains sigma for the old proof step and the goal map created by Proof_diffs.make_goal_map.

This function prints only the focused goals unless the corresponding option enable_unfocused_goal_printing is set. seeds is for printing dependent evars (mainly for emacs proof tree mode). shelf is from Proof.proof and is used to identify shelved goals in a message if there are no more subgoals but there are non-instantiated existential variables. stack is used to print summary info on unfocused goals.

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

pr_concl n ~diffs ~og_s sigma g prints the conclusion of the goal g using sigma. The output is labelled "subgoal n". If diffs is true, highlight the differences between the old conclusion, og_s, and g+sigma. og_s is a record containing the old goal and sigma, e.g. { it = g ; sigma = sigma }.

val pr_open_subgoals_diff : ?⁠quiet:bool -> ?⁠diffs:bool -> ?⁠oproof:Proof.t -> Proof.t -> Pp.t

pr_open_subgoals_diff ~quiet ~diffs ~oproof proof shows the context for proof as used by, for example, coqtop. The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their conclusions. If diffs is true, highlight the differences between the old proof, oproof, and proof. quiet disables printing messages as Feedback.

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

Declarations for the "Print Assumption" command

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 : Stdlib.Set.S with type ContextObjectSet.elt = context_object
module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet
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