coq-core 8.17.1 · OCaml Package

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

val print_goal_tag_opt_name : string list

Terms

Printers for terms.

The "lconstr" variant does not require parentheses to isolate the expression from the surrounding context (for instance 3 + 4 will be written 3 + 4). The "constr" variant (w/o "l") enforces parentheses whenever the term is not an atom (for instance, 3 will be written 3 but 3 + 4 will be written (3 + 4).

~inctx:true indicates that the term is intended to be printed in a context where its type is known so that a head coercion would be skipped, or implicit arguments inferable from the context will not be made explicit. For instance, if foo is declared as a coercion, foo bar will be printed as bar if inctx is true and as foo bar otherwise.

~scope:some_scope_name indicates that the head of the term is intended to be printed in scope some_scope_name. It defaults to None.

~impargs:some_list_of_binding_kind indicates the implicit arguments of the external quatification. Only used for printing types (not terms), and at toplevel (only "l" versions). It defaults to None.

~lax:true is for debugging purpose. It defaults to ~lax:false.

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

Same, but resilient to Nametab errors. Prints fully-qualified names when shortest_qualid_of_global has failed. Prints "??" in case of remaining issues (such as reference not in env).

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

Printers for types. Types are printed in scope "type_scope" and under the constraint of being of type a sort.

The "ltype" variant does not require parentheses to isolate the expression from the surrounding context (for instance nat * bool will be written nat * bool). The "type" variant (w/o "l") enforces parentheses whenever the term is not an atom (for instance, nat will be written nat but nat * bool will be written (nat * bool).

~goal_concl_style:true tells to print the type the same way as command Show would print a goal. Concretely, it means that all names of goal/section variables and all names of variables referred by de Bruijn indices (if any) in the given environment and all short names of global definitions of the current module must be avoided while printing bound variables. Otherwise, short names of global definitions are printed qualified and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided.

~lax:true is for debugging purpose.

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

Universe constraints

val pr_universe_instance : Evd.evar_map -> Univ.Instance.t -> Pp.t

val pr_universe_instance_constraints : 
  Evd.evar_map ->
  Univ.Instance.t ->
  Univ.Constraints.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.AbstractContext.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.AbstractContext.t ->
  UnivNames.univ_name_list option ->
  UnivNames.universe_binders * Names.Id.t Univ.Level.Map.t

universe_binders_with_opt_names ref l

If l is Some univs return the universe binders naming the bound levels of ref by univs (generating names for Anonymous). May error if the lengths mismatch.

Otherwise return the bound universe names registered for ref.

Inefficient on large contexts due to name generation.

Printing global references using names as short as possible

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 : Environ.env -> 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 : Tacred.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

Contexts

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

Predicates

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

Proofs, these functions obey Hyps Limit and Compact contexts.

val pr_open_subgoals : ?quiet:bool -> ?diffs:Proof.t option -> Proof.t -> Pp.t

pr_open_subgoals ~quiet ?diffs 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 Some oproof, highlight the differences between the old proof oproof, and proof. quiet disables printing messages as Feedback.

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:Evar.t list ->
  given_up:Evar.t 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

type axiom =

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

val print_goal_names : unit -> bool

Tells if flag "Printing Goal Names" is activated

module Debug : sig ... end

Debug printers

package coq-core