package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type 'a grammar_tactic_prod_item_expr =
  1. | TacTerm of string
  2. | TacNonTerm of ('a * Names.Id.t option) Loc.located
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
val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) Genarg.genarg_type -> 'a raw_extra_genarg_printer -> unit
type pp_tactic = {
  1. pptac_level : int;
  2. pptac_prods : grammar_terminals;
}
val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t
val declare_notation_tactic_pprule : Names.KerName.t -> pp_tactic -> unit
val pr_with_occurrences : ('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
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)) -> ('a, 'b, 'c) Genredexpr.red_expr_gen -> Pp.t
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) -> ('a, 'b, 'c) Genredexpr.may_eval -> Pp.t
val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t
val pr_evaluable_reference_env : Environ.env -> Tacred.evaluable_global_reference -> Pp.t
val pr_quantified_hypothesis : Tactypes.quantified_hypothesis -> Pp.t
val pr_in_clause : ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
val pr_clauses : bool option -> ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
val pr_raw_extend : Environ.env -> Evd.evar_map -> int -> Tacexpr.ml_tactic_entry -> Tacexpr.raw_tactic_arg list -> Pp.t
val pr_glob_extend : Environ.env -> int -> Tacexpr.ml_tactic_entry -> Tacexpr.glob_tactic_arg list -> Pp.t
val pr_extend : (Geninterp.Val.t -> Pp.t) -> int -> Tacexpr.ml_tactic_entry -> Geninterp.Val.t list -> Pp.t
val pr_alias_key : Names.KerName.t -> Pp.t
val pr_alias : (Geninterp.Val.t -> Pp.t) -> int -> Names.KerName.t -> Geninterp.Val.t list -> Pp.t
val pr_ltac_constant : Tacexpr.ltac_constant -> Pp.t
val pr_glob_tactic : Environ.env -> Tacexpr.glob_tactic_expr -> Pp.t
val pr_hintbases : string list option -> Pp.t
val pr_auto_using : ('constr -> Pp.t) -> 'constr list -> Pp.t
val pr_match_pattern : ('a -> Pp.t) -> 'a Tacexpr.match_pattern -> Pp.t
val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('b, 'a) Tacexpr.match_rule -> Pp.t
val make_constr_printer : (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'a -> Pp.t) -> 'a Genprint.top_printer
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct