package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module PrinterSource

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

Sourceval pr_in_comment : Pp.t -> Pp.t

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.

Sourceval pr_constr_env : ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
Sourceval pr_lconstr_env : ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> 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).

Sourceval safe_pr_constr_env : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
Sourceval safe_pr_lconstr_env : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t
Sourceval safe_extern_wrapper : (Environ.env -> Evd.evar_map -> 'a -> 'b) -> Environ.env -> Evd.evar_map -> 'a -> 'b option
Sourceval pr_econstr_env : ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t
Sourceval pr_leconstr_env : ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> EConstr.t -> Pp.t
Sourceval pr_econstr_n_env : ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t
Sourceval pr_etype_env : ?goal_concl_style:bool -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
Sourceval pr_letype_env : ?goal_concl_style:bool -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t
Sourceval pr_constr_under_binders_env : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
Sourceval pr_lconstr_under_binders_env : ?flags:PrintingFlags.t -> 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.

Sourceval pr_ltype_env : ?goal_concl_style:bool -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> Constr.types -> Pp.t
Sourceval pr_type_env : ?goal_concl_style:bool -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constr.types -> Pp.t
Sourceval pr_closed_glob_n_env : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Ltac_pretype.closed_glob_constr -> Pp.t
Sourceval pr_closed_glob_env : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
Sourceval pr_closed_lglob_env : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t
Sourceval pr_lglob_constr_env : ?flags:PrintingFlags.Extern.t -> Environ.env -> Evd.evar_map -> 'a Glob_term.glob_constr_g -> Pp.t
Sourceval pr_lconstr_pattern_env : ?flags:PrintingFlags.Extern.t -> Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
Sourceval pr_uninstantiated_lconstr_pattern_env : ?flags:PrintingFlags.Extern.t -> Environ.env -> Evd.evar_map -> Pattern.uninstantiated_pattern -> Pp.t
Sourceval pr_uninstantiated_constr_pattern_env : ?flags:PrintingFlags.Extern.t -> Environ.env -> Evd.evar_map -> Pattern.uninstantiated_pattern -> Pp.t
Sourceval pr_cases_pattern : ?flags:PrintingFlags.Extern.t -> Glob_term.cases_pattern -> Pp.t
Sourceval pr_sort : ?universes:bool -> ?qualities:bool -> Evd.evar_map -> Sorts.t -> Pp.t

Universe constraints

Sourceval pr_universe_instance : Evd.evar_map -> UVars.Instance.t -> Pp.t
Sourceval pr_abstract_universe_binder : Evd.evar_map -> UVars.AbstractContext.t -> Pp.t
Sourceval pr_universe_ctx : Evd.evar_map -> ?variance:UVars.Variance.t array -> UVars.UContext.t -> Pp.t
Sourceval pr_abstract_universe_ctx : Evd.evar_map -> ?variance:UVars.Variance.t array -> ?priv:Univ.ContextSet.t -> UVars.AbstractContext.t -> Pp.t
Sourceval pr_sort_context_set : Evd.evar_map -> UnivGen.sort_context_set -> Pp.t
Sourceval pr_universes : Evd.evar_map -> ?variance:UVars.Variance.t array -> ?priv:Univ.ContextSet.t -> Declarations.universes -> Pp.t

fill_names ref l

Generates names for Anonymous entries in ref. If l is Some univs, use first the names in univs, then those in ref and finally generated names. Can raise UniverseLengthMismatch. Inefficient on large contexts due to name generation.

Printing global references using names as short as possible

Sourceval pr_global_env : Names.Id.Set.t -> Names.GlobRef.t -> Pp.t
Sourceval pr_global : Names.GlobRef.t -> Pp.t
Sourceval pr_constant : Environ.env -> Names.Constant.t -> Pp.t
Sourceval pr_existential_key : Environ.env -> Evd.evar_map -> Evar.t -> Pp.t
Sourceval pr_existential : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constr.existential -> Pp.t
Sourceval pr_constructor : Environ.env -> Names.constructor -> Pp.t
Sourceval pr_inductive : Environ.env -> Names.inductive -> Pp.t
Sourceval pr_evaluable_reference : Environ.env -> Evaluable.t -> Pp.t
Sourceval pr_notation_interpretation_env : Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Pp.t

Contexts

Sourceval pr_context_unlimited : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_ne_context_of : Pp.t -> ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_ecompacted_decl : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Ppconstr.CompactedDecl.t -> Pp.t
Sourceval pr_named_context : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constr.named_context -> Pp.t
Sourceval pr_named_context_of : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_rel_context : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Constr.rel_context -> Pp.t
Sourceval pr_rel_context_of : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Pp.t
Sourceval pr_context_of : ?flags:PrintingFlags.t -> Environ.env -> Evd.evar_map -> Pp.t

Predicates

Sourceval pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t
Sourceval pr_cpred : Names.Cpred.t -> Pp.t
Sourceval pr_idpred : Names.Id.Pred.t -> Pp.t
Sourceval pr_prpred : Names.PRpred.t -> Pp.t
Sourceval pr_transparent_state : TransparentState.t -> Pp.t
Sourceval pr_evars_int : ?flags:PrintingFlags.t -> Evd.evar_map -> shelf:Evar.t list -> given_up:Evar.t list -> int -> Evd.undefined Evd.evar_info Evar.Map.t -> Pp.t
Sourceval pr_ne_evar_set : ?flags:PrintingFlags.t -> Pp.t -> Pp.t -> Evd.evar_map -> Evar.Set.t -> Pp.t

Declarations for the "Print Assumption" command

Sourceval print_all_assumptions : unit -> bool
Sourcetype 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
  6. | IndicesNotMattering of Names.MutInd.t
Sourcetype context_object =
  1. | Variable of Names.Id.t
  2. | Axiom of axiom * (Names.GlobRef.t * Constr.rel_context * Constr.types) list
  3. | Opaque of Names.Constant.t
  4. | Transparent of Names.Constant.t
Sourcetype theory_assumptions = {
  1. has_impredicative_set : bool;
  2. has_rewrite_rules : bool;
  3. has_type_in_type : bool;
}
Sourceval pr_typing_flags : Declarations.typing_flags -> Pp.t
Sourcemodule Debug : sig ... end

Debug printers