Tacinterp (rocq-runtime.Ltac

val ltac_trace_info : Tacexpr.ltac_stack Exninfo.t

module TacStore = Tacenv.TacStore

type interp_sign = Tacenv.interp_sign = {

lfun : Geninterp.Val.t Names.Id.Map.t;

poly : PolyFlags.t;

extra : TacStore.t;

}

Signature for interpretation: val\_interp and interpretation functions

module Value : sig ... end

type value = Value.t

Values for interpretation

val f_avoid_ids : Names.Id.Set.t TacStore.field

val f_debug : Tactic_debug.debug_info TacStore.field

val extract_loc : interp_sign -> Loc.t option

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 -> interp_sign -> Ltac_pretype.closed_glob_constr -> EConstr.constr Tactypes.delayed_open

Adds an interpretation function for extra generic arguments

val interp_genarg : (_, 'glb, 'top) Genarg.genarg_type -> interp_sign -> 'glb -> 'top Ftactic.t

val generic_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 -> Redexpr.glob_red_expr -> Evd.evar_map * Redexpr.red_expr

Interprets redexp arguments

val interp_strategy : interp_sign -> Environ.env -> Evd.evar_map -> Tacexpr.glob_strategy -> Rewrite.strategy

Interprets tactic expressions

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

Initial call for interpretation

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 -> Tacarg.tacvalue -> unit Proofview.tactic

val tactic_of_val : interp_sign -> Value.t -> unit Proofview.tactic

Globalization + interpretation

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

Internals that can be useful for syntax extensions.

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 interp_ident : interp_sign -> Environ.env -> Evd.evar_map -> Names.Id.t -> Names.Id.t

val interp_intro_pattern : interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t -> Tactypes.intro_pattern

val default_ist : unit -> interp_sign

Empty ist with debug set on the current value.

module Register : sig ... end