Module Ltac_plugin.Tacinterp

val ltac_trace_info : Tacexpr.ltac_trace Exninfo.t
module Value : sig ... end
type value = Value.t

Values for interpretation

module TacStore : Store.S with type t = Geninterp.TacStore.t and type 'a field = 'a Geninterp.TacStore.field
type interp_sign = Geninterp.interp_sign = {
lfun : value Names.Id.Map.t;
poly : bool;
extra : TacStore.t;
}

Signature for interpretation: val\_interp and interpretation functions

val f_avoid_ids : Names.Id.Set.t TacStore.field
val f_debug : Tactic_debug.debug_info TacStore.field
val extract_ltac_constr_values : interp_sign -> Environ.env -> Ltac_pretype.constr_under_binders Names.Id.Map.t

Given an interpretation signature, extract all values which are coercible to a constr.

val set_debug : Tactic_debug.debug_info -> unit

Sets the debugger mode

val get_debug : unit -> Tactic_debug.debug_info

Gives the state of debug

val type_uconstr : ?⁠flags:Pretyping.inference_flags -> ?⁠expected_type:Pretyping.typing_constraint -> Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> EConstr.constr Tactypes.delayed_open
val interp_genarg : interp_sign -> Genarg.glob_generic_argument -> Value.t Ftactic.t
val val_interp : interp_sign -> Tacexpr.glob_tactic_expr -> (value -> unit Proofview.tactic) -> unit Proofview.tactic

Interprets any expression

val interp_ltac_constr : interp_sign -> Tacexpr.glob_tactic_expr -> (EConstr.constr -> unit Proofview.tactic) -> unit Proofview.tactic

Interprets an expression that evaluates to a constr

val interp_red_expr : interp_sign -> Environ.env -> Evd.evar_map -> Tacexpr.glob_red_expr -> Evd.evar_map * Redexpr.red_expr

Interprets redexp arguments

val interp_redexp : Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr

Interprets redexp arguments from a raw one

val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> Names.lident -> Names.Id.t
val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?⁠kind:Pretyping.typing_constraint -> ?⁠pattern_mode:bool -> Genintern.glob_constr_and_expr -> Ltac_pretype.closed_glob_constr
val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Ltac_pretype.closed_glob_constr
val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Evd.evar_map * EConstr.constr
val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr Tactypes.bindings -> Evd.evar_map * EConstr.constr Tactypes.bindings
val interp_open_constr : ?⁠expected_type:Pretyping.typing_constraint -> ?⁠flags:Pretyping.inference_flags -> interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Evd.evar_map * EConstr.constr
val interp_open_constr_with_classes : ?⁠expected_type:Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Evd.evar_map * EConstr.constr
val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr Tactypes.with_bindings -> Evd.evar_map * EConstr.constr Tactypes.with_bindings
val eval_tactic : Tacexpr.glob_tactic_expr -> unit Proofview.tactic
val eval_tactic_ist : interp_sign -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic

Same as eval_tactic, but with the provided interp_sign.

val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic
val interp_tac_gen : value Names.Id.Map.t -> Names.Id.Set.t -> Tactic_debug.debug_info -> Tacexpr.raw_tactic_expr -> unit Proofview.tactic
val interp : Tacexpr.raw_tactic_expr -> unit Proofview.tactic
type ltac_expr = {
global : bool;
ast : Tacexpr.raw_tactic_expr;
}

Hides interpretation for pretty-print

val hide_interp : ltac_expr -> ComTactic.interpretable
val interp_ltac_var : (value -> 'a) -> interp_sign -> (Environ.env * Evd.evar_map) option -> Names.lident -> 'a
val interp_int : interp_sign -> Names.lident -> int
val interp_int_or_var : interp_sign -> int Locus.or_var -> int
val default_ist : unit -> Geninterp.interp_sign

Empty ist with debug set on the current value.