Module `Ltac_plugin.Tacexpr`

type ltac_constant = Names.KerName.t

type direction_flag = bool

type lazy_flag =

| General
| Select
| Once

type global_flag =

| TacGlobal
| TacLocal

type evars_flag = bool

type rec_flag = bool

type advanced_flag = bool

type letin_flag = bool

type clear_flag = bool option

type check_flag = bool

type ('c, 'd, 'id) inversion_strength =

| NonDepInversion of Inv.inversion_kind * 'id list * 'd Tactypes.or_and_intro_pattern_expr CAst.t Locus.or_var option
| DepInversion of Inv.inversion_kind * 'c option * 'd Tactypes.or_and_intro_pattern_expr CAst.t Locus.or_var option
| InversionUsing of 'c * 'id list

type 'id message_token =

| MsgString of string
| MsgInt of int
| MsgIdent of 'id

type ('dconstr, 'id) induction_clause =
  'dconstr Tactypes.with_bindings Tactics.destruction_arg
  * (Namegen.intro_pattern_naming_expr CAst.t option
     * 'dconstr Tactypes.or_and_intro_pattern_expr CAst.t Locus.or_var option)
  * 'id Locus.clause_expr option

type ('constr, 'dconstr, 'id) induction_clause_list =
  ('dconstr, 'id) induction_clause list * 'constr Tactypes.with_bindings option

type 'a with_bindings_arg = clear_flag * 'a Tactypes.with_bindings

type 'a match_pattern =

| Term of 'a
| Subterm of Names.Id.t option * 'a

type 'a match_context_hyps =

| Hyp of Names.lname * 'a match_pattern
| Def of Names.lname * 'a match_pattern * 'a match_pattern

type ('a, 't) match_rule =

| Pat of 'a match_context_hyps list * 'a match_pattern * 't
| All of 't

type ml_tactic_name = {

mltac_plugin : string;
(*
Name of the plugin where the tactic is defined, typically coming from a DECLARE PLUGIN statement in the source.
*)
mltac_tactic : string;
(*
Name of the tactic entry where the tactic is defined, typically found after the TACTIC EXTEND statement in the source.
*)

}

Extension indentifiers for the TACTIC EXTEND mechanism.

type ml_tactic_entry = {

mltac_name : ml_tactic_name;
mltac_index : int;

}

type open_constr_expr = unit * Constrexpr.constr_expr

Composite types

type open_glob_constr = unit * Genintern.glob_constr_and_expr

type intro_pattern =
  Tactypes.delayed_open_constr Tactypes.intro_pattern_expr CAst.t

type intro_patterns =
  Tactypes.delayed_open_constr Tactypes.intro_pattern_expr CAst.t list

type or_and_intro_pattern =
  Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr CAst.t

type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t

Generic expressions for atomic tactics

type 'a gen_atomic_tactic_expr =

| TacIntroPattern of evars_flag * 'dtrm Tactypes.intro_pattern_expr CAst.t list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * ('nam * 'dtrm Tactypes.intro_pattern_expr CAst.t option) list
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm Tactypes.with_bindings option
| TacCase of evars_flag * 'trm with_bindings_arg
| TacMutualFix of Names.Id.t * int * (Names.Id.t * int * 'trm) list
| TacMutualCofix of Names.Id.t * (Names.Id.t * 'trm) list
| TacAssert of evars_flag * bool * 'tacexpr option option * 'dtrm Tactypes.intro_pattern_expr CAst.t option * 'trm
| TacGeneralize of (('occvar Locus.occurrences_gen * 'trm) * Names.Name.t) list
| TacLetTac of evars_flag * Names.Name.t * 'trm * 'nam Locus.clause_expr * letin_flag * Namegen.intro_pattern_naming_expr CAst.t option
| TacInductionDestruct of rec_flag * evars_flag * ('trm, 'dtrm, 'nam) induction_clause_list
| TacReduce of ('trm, 'cst, 'rpat, 'occvar) Genredexpr.red_expr_gen * 'nam Locus.clause_expr
| TacChange of check_flag * 'rpat option * 'dtrm * 'nam Locus.clause_expr
| TacRewrite of evars_flag * (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam Locus.clause_expr * 'tacexpr option
| TacInversion of ('trm, 'dtrm, 'nam) inversion_strength * Tactypes.quantified_hypothesis


  constraint
    'a =
    < term : 'trm
    ; dterm : 'dtrm
    ; pattern : 'pat
    ; red_pattern : 'rpat
    ; constant : 'cst
    ; reference : 'ref
    ; name : 'nam
    ; occvar : 'occvar
    ; tacexpr : 'tacexpr
    ; level : 'lev >

Possible arguments of a tactic definition

type 'a gen_tactic_arg =

| TacGeneric of string option * 'lev Genarg.generic_argument
| ConstrMayEval of ('trm, 'cst, 'rpat, 'occvar) Genredexpr.may_eval
| Reference of 'ref
| TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
| TacFreshId of string Locus.or_var list
| Tacexp of 'tacexpr
| TacPretype of 'trm
| TacNumgoals


  constraint
    'a =
    < term : 'trm
    ; dterm : 'dtrm
    ; pattern : 'pat
    ; red_pattern : 'rpat
    ; constant : 'cst
    ; reference : 'ref
    ; name : 'nam
    ; occvar : 'occvar
    ; tacexpr : 'tacexpr
    ; level : 'lev >

Generic ltac expressions. 't : terms, 'p : patterns, 'c : constants, 'i : inductive, 'r : ltac refs, 'n : idents, 'l : levels

and 'a gen_tactic_expr_r =

| TacAtom of 'a gen_atomic_tactic_expr
| TacThen of 'a gen_tactic_expr * 'a gen_tactic_expr
| TacDispatch of 'a gen_tactic_expr list
| TacExtendTac of 'a gen_tactic_expr array * 'a gen_tactic_expr * 'a gen_tactic_expr array
| TacThens of 'a gen_tactic_expr * 'a gen_tactic_expr list
| TacThens3parts of 'a gen_tactic_expr * 'a gen_tactic_expr array * 'a gen_tactic_expr * 'a gen_tactic_expr array
| TacFirst of 'a gen_tactic_expr list
| TacSolve of 'a gen_tactic_expr list
| TacTry of 'a gen_tactic_expr
| TacOr of 'a gen_tactic_expr * 'a gen_tactic_expr
| TacOnce of 'a gen_tactic_expr
| TacExactlyOnce of 'a gen_tactic_expr
| TacIfThenCatch of 'a gen_tactic_expr * 'a gen_tactic_expr * 'a gen_tactic_expr
| TacOrelse of 'a gen_tactic_expr * 'a gen_tactic_expr
| TacDo of int Locus.or_var * 'a gen_tactic_expr
| TacTimeout of int Locus.or_var * 'a gen_tactic_expr
| TacTime of string option * 'a gen_tactic_expr
| TacRepeat of 'a gen_tactic_expr
| TacProgress of 'a gen_tactic_expr
| TacAbstract of 'a gen_tactic_expr * Names.Id.t option
| TacId of 'n message_token list
| TacFail of global_flag * int Locus.or_var * 'n message_token list
| TacLetIn of rec_flag * (Names.lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr
| TacMatch of lazy_flag * 'a gen_tactic_expr * ('p, 'a gen_tactic_expr) match_rule list
| TacMatchGoal of lazy_flag * direction_flag * ('p, 'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg
| TacSelect of Goal_select.t * 'a gen_tactic_expr
| TacML of ml_tactic_entry * 'a gen_tactic_arg list
| TacAlias of Names.KerName.t * 'a gen_tactic_arg list


  constraint
    'a =
    < term : 't
    ; dterm : 'dtrm
    ; pattern : 'p
    ; red_pattern : 'rp
    ; constant : 'c
    ; reference : 'r
    ; name : 'n
    ; occvar : 'occvar
    ; tacexpr : 'tacexpr
    ; level : 'l >

and 'a gen_tactic_expr = 'a gen_tactic_expr_r CAst.t
  constraint
    'a =
    < term : 't
    ; dterm : 'dtrm
    ; pattern : 'p
    ; red_pattern : 'rp
    ; constant : 'c
    ; reference : 'r
    ; name : 'n
    ; occvar : 'occvar
    ; tacexpr : 'tacexpr
    ; level : 'l >

and 'a gen_tactic_fun_ast = Names.Name.t list * 'a gen_tactic_expr
  constraint
    'a =
    < term : 't
    ; dterm : 'dtrm
    ; pattern : 'p
    ; red_pattern : 'rp
    ; constant : 'c
    ; reference : 'r
    ; name : 'n
    ; occvar : 'occvar
    ; tacexpr : 'te
    ; level : 'l >

Globalized tactics

type g_trm = Genintern.glob_constr_and_expr

type g_pat = Genintern.glob_constr_pattern_and_expr

type g_cst = Evaluable.t Genredexpr.and_short_name Locus.or_var

type g_ref = ltac_constant Loc.located Locus.or_var

type g_nam = Names.lident

type g_occvar = int Locus.or_var

type g_dispatch =
  < term : g_trm
  ; dterm : g_trm
  ; pattern : g_pat
  ; red_pattern : g_trm
  ; constant : g_cst
  ; reference : g_ref
  ; name : g_nam
  ; occvar : g_occvar
  ; tacexpr : glob_tactic_expr
  ; level : Genarg.glevel >

and glob_tactic_expr = g_dispatch gen_tactic_expr

type glob_atomic_tactic_expr = g_dispatch gen_atomic_tactic_expr

type glob_tactic_arg = g_dispatch gen_tactic_arg

Raw tactics

type r_ref = Libnames.qualid

type r_nam = Names.lident

type r_lev = Genarg.rlevel

type r_occvar = int Locus.or_var

type r_dispatch =
  < term : Genredexpr.r_trm
  ; dterm : Genredexpr.r_trm
  ; pattern : Genredexpr.r_pat
  ; red_pattern : Genredexpr.r_pat
  ; constant : Genredexpr.r_cst
  ; reference : r_ref
  ; name : r_nam
  ; occvar : r_occvar
  ; tacexpr : raw_tactic_expr
  ; level : Genarg.rlevel >

and raw_tactic_expr = r_dispatch gen_tactic_expr

type raw_atomic_tactic_expr = r_dispatch gen_atomic_tactic_expr

type raw_tactic_arg = r_dispatch gen_tactic_arg

Interpreted tactics

type t_trm = EConstr.constr

type t_pat = Pattern.constr_pattern

type t_cst = Evaluable.t

type t_ref = ltac_constant Loc.located

type t_nam = Names.Id.t

type t_occvar = int

type t_dispatch =
  < term : t_trm
  ; dterm : g_trm
  ; pattern : t_pat
  ; red_pattern : t_pat
  ; constant : t_cst
  ; reference : t_ref
  ; name : t_nam
  ; occvar : t_occvar
  ; tacexpr : unit
  ; level : Genarg.tlevel >

type atomic_tactic_expr = t_dispatch gen_atomic_tactic_expr

Misc

type raw_strategy =
  (Constrexpr.constr_expr, Genredexpr.raw_red_expr, Names.lident)
    Rewrite.strategy_ast

type glob_strategy =
  (Genintern.glob_constr_and_expr, Genredexpr.glob_red_expr, Names.Id.t)
    Rewrite.strategy_ast

Traces

type ltac_call_kind =

| LtacMLCall of glob_tactic_expr
| LtacNotationCall of Names.KerName.t
| LtacNameCall of ltac_constant
| LtacAtomCall of glob_atomic_tactic_expr
| LtacVarCall of Names.KerName.t option * Names.Id.t * glob_tactic_expr
| LtacConstrInterp of Environ.env * Evd.evar_map * Glob_term.glob_constr * Ltac_pretype.ltac_var_map

type ltac_stack = ltac_call_kind Loc.located list

type ltac_trace = ltac_stack * Geninterp.Val.t Names.Id.Map.t list

type tacdef_body =

| TacticDefinition of Names.lident * raw_tactic_expr
| TacticRedefinition of Libnames.qualid * raw_tactic_expr

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tacexpr/index.html

Module `Ltac_plugin.Tacexpr`

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tacexpr/index.html

Module Ltac_plugin.Tacexpr

Module `Ltac_plugin.Tacexpr`