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 ('a, 'b) location
=
|
HypLocation of 'a
|
ConclLocation of 'b
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
=
{
}
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
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) option
|
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 ('trm Locus.with_occurrences * 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, 'pat) Genredexpr.red_expr_gen * 'nam Locus.clause_expr
|
TacChange of check_flag * 'pat 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; constant : 'cst; reference : 'ref; name : 'nam; tacexpr : 'tacexpr; level : 'lev; >
type 'a gen_tactic_arg
=
|
TacGeneric of 'lev Genarg.generic_argument
|
ConstrMayEval of ('trm, 'cst, 'pat) 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; constant : 'cst; reference : 'ref; name : 'nam; tacexpr : 'tacexpr; level : 'lev; >
and 'a gen_tactic_expr
=
constraint 'a = < term : 't; dterm : 'dtrm; pattern : 'p; constant : 'c; reference : 'r; name : 'n; 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; constant : 'c; reference : 'r; name : 'n; tacexpr : 'te; level : 'l; >
type g_trm
= Genintern.glob_constr_and_expr
type g_pat
= Genintern.glob_constr_pattern_and_expr
type g_cst
= Names.evaluable_global_reference Genredexpr.and_short_name Locus.or_var
type g_ref
= ltac_constant Loc.located Locus.or_var
type g_nam
= Names.lident
type g_dispatch
= < term : g_trm; dterm : g_trm; pattern : g_pat; constant : g_cst; reference : g_ref; name : g_nam; 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
type r_ref
= Libnames.qualid
type r_nam
= Names.lident
type r_lev
= Genarg.rlevel
type r_dispatch
= < term : Genredexpr.r_trm; dterm : Genredexpr.r_trm; pattern : Genredexpr.r_pat; constant : Genredexpr.r_cst; reference : r_ref; name : r_nam; 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
type t_trm
= EConstr.constr
type t_pat
= Pattern.constr_pattern
type t_cst
= Names.evaluable_global_reference
type t_ref
= ltac_constant Loc.located
type t_nam
= Names.Id.t
type t_dispatch
= < term : t_trm; dterm : g_trm; pattern : t_pat; constant : t_cst; reference : t_ref; name : t_nam; tacexpr : unit; level : Genarg.tlevel; >
type atomic_tactic_expr
= t_dispatch gen_atomic_tactic_expr
type raw_red_expr
= (Genredexpr.r_trm, Genredexpr.r_cst, Genredexpr.r_pat) Genredexpr.red_expr_gen
type glob_red_expr
= (g_trm, g_cst, g_pat) Genredexpr.red_expr_gen
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.Id.t * glob_tactic_expr
|
LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
type ltac_trace
= ltac_call_kind Loc.located list
type tacdef_body
=
|
TacticDefinition of Names.lident * raw_tactic_expr
|
TacticRedefinition of Libnames.qualid * raw_tactic_expr