Module `Ltac_plugin.Tacinterp`Source

Sourceval ltac_trace_info : Tacexpr.ltac_stack Exninfo.t

Sourcemodule TacStore = Tacenv.TacStore

Sourcetype 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

Sourcemodule Value : sig ... end

Sourcetype value = Value.t

Values for interpretation

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

Sourceval f_debug : Tactic_debug.debug_info TacStore.field

Sourceval extract_loc : interp_sign -> Loc.t option

Source

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.

Sourceval set_debug : Tactic_debug.debug_info -> unit

Sets the debugger mode

Sourceval get_debug : unit -> Tactic_debug.debug_info

Gives the state of debug

Source

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

Source

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

Source

val generic_interp_genarg : 
  interp_sign ->
  Genarg.glob_generic_argument ->
  Value.t Ftactic.t

Source

val val_interp : 
  interp_sign ->
  Tacexpr.glob_tactic_expr ->
  (value -> unit Proofview.tactic) ->
  unit Proofview.tactic

Interprets any expression

Source

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

Source

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

Interprets redexp arguments

Source

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

Interprets tactic expressions

Source

val interp_hyp : 
  interp_sign ->
  Environ.env ->
  Evd.evar_map ->
  Names.lident ->
  Names.Id.t

Source

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

Source

val interp_uconstr : 
  interp_sign ->
  Environ.env ->
  Evd.evar_map ->
  Genintern.glob_constr_and_expr ->
  Ltac_pretype.closed_glob_constr

Source

val interp_constr_gen : 
  Pretyping.typing_constraint ->
  interp_sign ->
  Environ.env ->
  Evd.evar_map ->
  Genintern.glob_constr_and_expr ->
  Evd.evar_map * EConstr.constr

Source

val interp_bindings : 
  interp_sign ->
  Environ.env ->
  Evd.evar_map ->
  Genintern.glob_constr_and_expr Tactypes.bindings ->
  Evd.evar_map * EConstr.constr Tactypes.bindings

Source

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

Source

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

Source

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

Sourceval eval_tactic : Tacexpr.glob_tactic_expr -> unit Proofview.tactic

Source

val eval_tactic_ist : 
  interp_sign ->
  Tacexpr.glob_tactic_expr ->
  unit Proofview.tactic

Same as eval_tactic, but with the provided interp_sign.

Sourceval tactic_of_value : interp_sign -> Tacarg.tacvalue -> unit Proofview.tactic

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

Globalization + interpretation

Source

val interp_tac_gen : 
  value Names.Id.Map.t ->
  Names.Id.Set.t ->
  Tactic_debug.debug_info ->
  Tacexpr.raw_tactic_expr ->
  unit Proofview.tactic

Sourceval interp : Tacexpr.raw_tactic_expr -> unit Proofview.tactic

Sourcetype ltac_expr = {

global : bool;
ast : Tacexpr.raw_tactic_expr;

}

Hides interpretation for pretty-print

Sourceval hide_interp : ltac_expr -> ComTactic.interpretable

Internals that can be useful for syntax extensions.

Source

val interp_ltac_var : 
  (value -> 'a) ->
  interp_sign ->
  (Environ.env * Evd.evar_map) option ->
  Names.lident ->
  'a

Sourceval interp_int : interp_sign -> Names.lident -> int

Sourceval interp_int_or_var : interp_sign -> int Locus.or_var -> int

Source

val interp_ident : 
  interp_sign ->
  Environ.env ->
  Evd.evar_map ->
  Names.Id.t ->
  Names.Id.t

Source

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

Sourceval default_ist : unit -> interp_sign

Empty ist with debug set on the current value.

Sourcemodule Register : sig ... end

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tacinterp/index.html

Module `Ltac_plugin.Tacinterp`Source

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tacinterp/index.html

Module Ltac_plugin.TacinterpSource

dune-project
Dependency

Module `Ltac_plugin.Tacinterp`Source