Module `Ltac_plugin.Pptactic`Source

This module implements pretty-printers for ltac_expr syntactic objects and their subcomponents.

Sourcetype 'a grammar_tactic_prod_item_expr =

| TacTerm of string
| TacNonTerm of ('a * Names.Id.t option) Loc.located

type 'a raw_extra_genarg_printer =
  Environ.env ->
  Evd.evar_map ->
  (Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) ->
  (Environ.env ->
    Evd.evar_map ->
    Constrexpr.entry_relative_level ->
    Tacexpr.raw_tactic_expr ->
    Pp.t) ->
  'a ->
  Pp.t

Source

type 'a glob_extra_genarg_printer =
  Environ.env ->
  Evd.evar_map ->
  (Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) ->
  (Environ.env ->
    Evd.evar_map ->
    Constrexpr.entry_relative_level ->
    Tacexpr.glob_tactic_expr ->
    Pp.t) ->
  'a ->
  Pp.t

Source

type 'a extra_genarg_printer =
  Environ.env ->
  Evd.evar_map ->
  (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
  (Environ.env ->
    Evd.evar_map ->
    Constrexpr.entry_relative_level ->
    Geninterp.Val.t ->
    Pp.t) ->
  'a ->
  Pp.t

Source

type 'a raw_extra_genarg_printer_with_level =
  Environ.env ->
  Evd.evar_map ->
  (Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Pp.t) ->
  (Environ.env ->
    Evd.evar_map ->
    Constrexpr.entry_relative_level ->
    Tacexpr.raw_tactic_expr ->
    Pp.t) ->
  Constrexpr.entry_relative_level ->
  'a ->
  Pp.t

Source

type 'a glob_extra_genarg_printer_with_level =
  Environ.env ->
  Evd.evar_map ->
  (Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Pp.t) ->
  (Environ.env ->
    Evd.evar_map ->
    Constrexpr.entry_relative_level ->
    Tacexpr.glob_tactic_expr ->
    Pp.t) ->
  Constrexpr.entry_relative_level ->
  'a ->
  Pp.t

Source

type 'a extra_genarg_printer_with_level =
  Environ.env ->
  Evd.evar_map ->
  (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
  (Environ.env ->
    Evd.evar_map ->
    Constrexpr.entry_relative_level ->
    Geninterp.Val.t ->
    Pp.t) ->
  Constrexpr.entry_relative_level ->
  'a ->
  Pp.t

Source

val declare_extra_genarg_pprule : 
  ('a, 'b, 'c) Genarg.genarg_type ->
  'a raw_extra_genarg_printer ->
  'b glob_extra_genarg_printer ->
  'c extra_genarg_printer ->
  unit

Source

val declare_extra_genarg_pprule_with_level : 
  ('a, 'b, 'c) Genarg.genarg_type ->
  'a raw_extra_genarg_printer_with_level ->
  'b glob_extra_genarg_printer_with_level ->
  'c extra_genarg_printer_with_level ->
  Constrexpr.entry_relative_level ->
  Constrexpr.entry_relative_level ->
  unit

Source

type grammar_terminals =
  Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list

Sourcetype pp_tactic = {

pptac_level : int;
pptac_prods : grammar_terminals;

}

Sourceval pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t

Sourceval declare_notation_tactic_pprule : Names.KerName.t -> pp_tactic -> unit

Source

val pr_with_occurrences : 
  ('v -> Pp.t) ->
  ('a -> Pp.t) ->
  ('v Locus.occurrences_gen * 'a) ->
  Pp.t

Source

val pr_red_expr : 
  Environ.env ->
  Evd.evar_map ->
  ((Environ.env ->
   Evd.evar_map ->
   'a ->
   Pp.t)
   * (Environ.env ->
   Evd.evar_map ->
   'a ->
   Pp.t)
   * ('b ->
   Pp.t)
   * (Environ.env ->
   Evd.evar_map ->
   'c ->
   Pp.t)
   * ('occvar ->
   Pp.t)) ->
  ('a, 'b, 'c, 'occvar) Genredexpr.red_expr_gen ->
  Pp.t

Source

val pr_may_eval : 
  Environ.env ->
  Evd.evar_map ->
  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) ->
  ('b -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
  ('occvar -> Pp.t) ->
  ('a, 'b, 'c, 'occvar) Genredexpr.may_eval ->
  Pp.t

Sourceval pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t

Sourceval pr_evaluable_reference_env : Environ.env -> Evaluable.t -> Pp.t

Sourceval pr_quantified_hypothesis : Tactypes.quantified_hypothesis -> Pp.t

Sourceval pr_in_clause : ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t

Sourceval pr_clauses : bool option -> ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t

Source

val pr_raw_generic : 
  Environ.env ->
  Evd.evar_map ->
  Genarg.rlevel Genarg.generic_argument ->
  Pp.t

Source

val pr_glb_generic : 
  Environ.env ->
  Evd.evar_map ->
  Genarg.glevel Genarg.generic_argument ->
  Pp.t

Source

val pr_raw_extend : 
  Environ.env ->
  Evd.evar_map ->
  int ->
  Tacexpr.ml_tactic_entry ->
  Tacexpr.raw_tactic_arg list ->
  Pp.t

Source

val pr_glob_extend : 
  Environ.env ->
  int ->
  Tacexpr.ml_tactic_entry ->
  Tacexpr.glob_tactic_arg list ->
  Pp.t

Source

val pr_extend : 
  (Geninterp.Val.t -> Pp.t) ->
  int ->
  Tacexpr.ml_tactic_entry ->
  Geninterp.Val.t list ->
  Pp.t

Sourceval pr_alias_key : Names.KerName.t -> Pp.t

Source

val pr_alias : 
  (Geninterp.Val.t -> Pp.t) ->
  int ->
  Names.KerName.t ->
  Geninterp.Val.t list ->
  Pp.t

Sourceval pr_ltac_constant : Tacexpr.ltac_constant -> Pp.t

Source

val pr_raw_tactic : 
  Environ.env ->
  Evd.evar_map ->
  Tacexpr.raw_tactic_expr ->
  Pp.t

Source

val pr_raw_tactic_level : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.entry_relative_level ->
  Tacexpr.raw_tactic_expr ->
  Pp.t

Sourceval pr_glob_tactic : Environ.env -> Tacexpr.glob_tactic_expr -> Pp.t

Source

val pr_atomic_tactic : 
  Environ.env ->
  Evd.evar_map ->
  Tacexpr.atomic_tactic_expr ->
  Pp.t

Sourceval pr_hintbases : string list option -> Pp.t

Sourceval pr_auto_using : ('constr -> Pp.t) -> 'constr list -> Pp.t

Sourceval pr_match_pattern : ('a -> Pp.t) -> 'a Tacexpr.match_pattern -> Pp.t

Source

val pr_match_rule : 
  bool ->
  ('a -> Pp.t) ->
  ('b -> Pp.t) ->
  ('b, 'a) Tacexpr.match_rule ->
  Pp.t

Sourceval pr_value : Constrexpr.entry_relative_level -> Geninterp.Val.t -> Pp.t

Sourceval pp_ltac_call_kind : Tacexpr.ltac_call_kind -> Pp.t

Sourceval ltop : Constrexpr.entry_relative_level

Source

val make_constr_printer : 
  (Environ.env ->
    Evd.evar_map ->
    Constrexpr.entry_relative_level ->
    'a ->
    Pp.t) ->
  'a Genprint.top_printer

Sourceval ssr_loaded_hook : (unit -> bool) -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Pptactic/index.html

Module `Ltac_plugin.Pptactic`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Pptactic/index.html

Module Ltac_plugin.PptacticSource

Module `Ltac_plugin.Pptactic`Source