package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ltac_constant = Names.KerName.t
type direction_flag = bool
type lazy_flag =
  1. | General
  2. | Select
  3. | Once
type global_flag =
  1. | TacGlobal
  2. | 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 =
  1. | NonDepInversion of Inv.inversion_kind * 'id list * 'd Tactypes.or_and_intro_pattern_expr CAst.t Locus.or_var option
  2. | DepInversion of Inv.inversion_kind * 'c option * 'd Tactypes.or_and_intro_pattern_expr CAst.t Locus.or_var option
  3. | InversionUsing of 'c * 'id list
type 'id message_token =
  1. | MsgString of string
  2. | MsgInt of int
  3. | MsgIdent of 'id
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 =
  1. | Term of 'a
  2. | Subterm of Names.Id.t option * 'a
type 'a match_context_hyps =
  1. | Hyp of Names.lname * 'a match_pattern
  2. | Def of Names.lname * 'a match_pattern * 'a match_pattern
type ('a, 't) match_rule =
  1. | Pat of 'a match_context_hyps list * 'a match_pattern * 't
  2. | All of 't
type ml_tactic_name = {
  1. mltac_plugin : string;
    (*

    Name of the plugin where the tactic is defined, typically coming from a DECLARE PLUGIN statement in the source.

    *)
  2. 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 = {
  1. mltac_name : ml_tactic_name;
  2. 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_naming = Namegen.intro_pattern_naming_expr CAst.t

Generic expressions for atomic tactics

type 'a gen_atomic_tactic_expr =
  1. | TacIntroPattern of evars_flag * 'dtrm Tactypes.intro_pattern_expr CAst.t list
  2. | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * ('nam * 'dtrm Tactypes.intro_pattern_expr CAst.t option) list
  3. | TacElim of evars_flag * 'trm with_bindings_arg * 'trm Tactypes.with_bindings option
  4. | TacCase of evars_flag * 'trm with_bindings_arg
  5. | TacMutualFix of Names.Id.t * int * (Names.Id.t * int * 'trm) list
  6. | TacMutualCofix of Names.Id.t * (Names.Id.t * 'trm) list
  7. | TacAssert of evars_flag * bool * 'tacexpr option option * 'dtrm Tactypes.intro_pattern_expr CAst.t option * 'trm
  8. | TacGeneralize of (('occvar Locus.occurrences_gen * 'trm) * Names.Name.t) list
  9. | TacLetTac of evars_flag * Names.Name.t * 'trm * 'nam Locus.clause_expr * letin_flag * Namegen.intro_pattern_naming_expr CAst.t option
  10. | TacInductionDestruct of rec_flag * evars_flag * ('trm, 'dtrm, 'nam) induction_clause_list
  11. | TacReduce of ('trm, 'cst, 'rpat, 'occvar) Genredexpr.red_expr_gen * 'nam Locus.clause_expr
  12. | TacChange of check_flag * 'rpat option * 'dtrm * 'nam Locus.clause_expr
  13. | TacRewrite of evars_flag * (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam Locus.clause_expr * 'tacexpr option
  14. | 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 =
  1. | TacGeneric of string option * 'lev Genarg.generic_argument
  2. | ConstrMayEval of ('trm, 'cst, 'rpat, 'occvar) Genredexpr.may_eval
  3. | Reference of 'ref
  4. | TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
  5. | TacFreshId of string Locus.or_var list
  6. | Tacexp of 'tacexpr
  7. | TacPretype of 'trm
  8. | 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 =
  1. | TacAtom of 'a gen_atomic_tactic_expr
  2. | TacThen of 'a gen_tactic_expr * 'a gen_tactic_expr
  3. | TacDispatch of 'a gen_tactic_expr list
  4. | TacExtendTac of 'a gen_tactic_expr array * 'a gen_tactic_expr * 'a gen_tactic_expr array
  5. | TacThens of 'a gen_tactic_expr * 'a gen_tactic_expr list
  6. | TacThens3parts of 'a gen_tactic_expr * 'a gen_tactic_expr array * 'a gen_tactic_expr * 'a gen_tactic_expr array
  7. | TacFirst of 'a gen_tactic_expr list
  8. | TacSolve of 'a gen_tactic_expr list
  9. | TacTry of 'a gen_tactic_expr
  10. | TacOr of 'a gen_tactic_expr * 'a gen_tactic_expr
  11. | TacOnce of 'a gen_tactic_expr
  12. | TacExactlyOnce of 'a gen_tactic_expr
  13. | TacIfThenCatch of 'a gen_tactic_expr * 'a gen_tactic_expr * 'a gen_tactic_expr
  14. | TacOrelse of 'a gen_tactic_expr * 'a gen_tactic_expr
  15. | TacDo of int Locus.or_var * 'a gen_tactic_expr
  16. | TacTimeout of int Locus.or_var * 'a gen_tactic_expr
  17. | TacTime of string option * 'a gen_tactic_expr
  18. | TacRepeat of 'a gen_tactic_expr
  19. | TacProgress of 'a gen_tactic_expr
  20. | TacAbstract of 'a gen_tactic_expr * Names.Id.t option
  21. | TacId of 'n message_token list
  22. | TacFail of global_flag * int Locus.or_var * 'n message_token list
  23. | TacLetIn of rec_flag * (Names.lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr
  24. | TacMatch of lazy_flag * 'a gen_tactic_expr * ('p, 'a gen_tactic_expr) match_rule list
  25. | TacMatchGoal of lazy_flag * direction_flag * ('p, 'a gen_tactic_expr) match_rule list
  26. | TacFun of 'a gen_tactic_fun_ast
  27. | TacArg of 'a gen_tactic_arg
  28. | TacSelect of Goal_select.t * 'a gen_tactic_expr
  29. | TacML of ml_tactic_entry * 'a gen_tactic_arg list
  30. | 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_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_cst = Evaluable.t
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

Traces

type ltac_call_kind =
  1. | LtacMLCall of glob_tactic_expr
  2. | LtacNotationCall of Names.KerName.t
  3. | LtacNameCall of ltac_constant
  4. | LtacAtomCall of glob_atomic_tactic_expr
  5. | LtacVarCall of Names.KerName.t option * Names.Id.t * glob_tactic_expr
  6. | 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 =
  1. | TacticDefinition of Names.lident * raw_tactic_expr
  2. | TacticRedefinition of Libnames.qualid * raw_tactic_expr
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct