Tacinterp (coq-core.Ltac_plugin.Tacinterp)

val ltac_trace_info : Tacexpr.ltac_stack 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

Adds an interpretation function for extra generic arguments

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

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 -> 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 -> Geninterp.interp_sign

Empty ist with debug set on the current value.