Ltac_plugin.Tacinterpval ltac_trace_info : Tacexpr.ltac_stack Exninfo.tmodule Value : sig ... endtype value = Value.tValues for interpretation
module TacStore : Store.S with type t = Geninterp.TacStore.t and type 'a field = 'a Geninterp.TacStore.fieldtype 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.fieldval f_debug : Tactic_debug.debug_info TacStore.fieldval extract_ltac_constr_values : interp_sign -> Environ.env -> Ltac_pretype.constr_under_binders Names.Id.Map.tGiven an interpretation signature, extract all values which are coercible to a constr.
val set_debug : Tactic_debug.debug_info -> unitSets the debugger mode
val get_debug : unit -> Tactic_debug.debug_infoGives 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_openAdds an interpretation function for extra generic arguments
val interp_genarg : interp_sign -> Genarg.glob_generic_argument -> Value.t Ftactic.tval val_interp : interp_sign -> Tacexpr.glob_tactic_expr -> (value -> unit Proofview.tactic) -> unit Proofview.tacticInterprets any expression
val interp_ltac_constr : interp_sign -> Tacexpr.glob_tactic_expr -> (EConstr.constr -> unit Proofview.tactic) -> unit Proofview.tacticInterprets an expression that evaluates to a constr
val interp_red_expr : interp_sign -> Environ.env -> Evd.evar_map -> Genredexpr.glob_red_expr -> Evd.evar_map * Redexpr.red_exprInterprets redexp arguments
val interp_strategy : interp_sign -> Environ.env -> Evd.evar_map -> Tacexpr.glob_strategy -> Rewrite.strategyInterprets tactic expressions
val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> Names.lident -> Names.Id.tval 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_constrval interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Ltac_pretype.closed_glob_constrval interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr -> Evd.evar_map * EConstr.constrval interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr Tactypes.bindings -> Evd.evar_map * EConstr.constr Tactypes.bindingsval 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.constrval 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.constrval 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_bindingsInitial call for interpretation
val eval_tactic : Tacexpr.glob_tactic_expr -> unit Proofview.tacticval eval_tactic_ist : interp_sign -> Tacexpr.glob_tactic_expr -> unit Proofview.tacticSame as eval_tactic, but with the provided interp_sign.
val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tacticGlobalization + interpretation
val interp_tac_gen : value Names.Id.Map.t -> Names.Id.Set.t -> Tactic_debug.debug_info -> Tacexpr.raw_tactic_expr -> unit Proofview.tacticval interp : Tacexpr.raw_tactic_expr -> unit Proofview.tacticHides interpretation for pretty-print
val hide_interp : ltac_expr -> ComTactic.interpretableInternals that can be useful for syntax extensions.
val interp_ltac_var : (value -> 'a) -> interp_sign -> (Environ.env * Evd.evar_map) option -> Names.lident -> 'aval interp_int : interp_sign -> Names.lident -> intval interp_int_or_var : interp_sign -> int Locus.or_var -> intval interp_ident : interp_sign -> Environ.env -> Evd.evar_map -> Names.Id.t -> Names.Id.tval interp_intro_pattern : interp_sign -> Environ.env -> Evd.evar_map -> Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t -> Tactypes.intro_patternval default_ist : unit -> Geninterp.interp_signEmpty ist with debug set on the current value.