package coq

  1. Overview
  2. Docs
package coq
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 goal_selector = Goal_select.t =
  1. | SelectAlreadyFocused
    (*
    • deprecated Use constructors in [Goal_select]
    *)
  2. | SelectNth of int
    (*
    • deprecated Use constructors in [Goal_select]
    *)
  3. | SelectList of (int * int) list
    (*
    • deprecated Use constructors in [Goal_select]
    *)
  4. | SelectId of Names.Id.t
    (*
    • deprecated Use constructors in [Goal_select]
    *)
  5. | SelectAll
    (*
    • deprecated Use constructors in [Goal_select]
    *)
  • deprecated Use Vernacexpr.goal_selector
type !'a core_destruction_arg = 'a Tactics.core_destruction_arg =
  1. | ElimOnConstr of 'a
    (*
    • deprecated Use constructors in [Tactics]
    *)
  2. | ElimOnIdent of Names.lident
    (*
    • deprecated Use constructors in [Tactics]
    *)
  3. | ElimOnAnonHyp of int
    (*
    • deprecated Use constructors in [Tactics]
    *)
  • deprecated Use Tactics.core_destruction_arg
type !'a destruction_arg = clear_flag * 'a Tactics.core_destruction_arg
  • deprecated Use Tactics.destruction_arg
type inversion_kind = Inv.inversion_kind =
  1. | SimpleInversion
    (*
    • deprecated Use constructors in [Inv]
    *)
  2. | FullInversion
    (*
    • deprecated Use constructors in [Inv]
    *)
  3. | FullInversionClear
    (*
    • deprecated Use constructors in [Inv]
    *)
  • deprecated Use Tactics.inversion_kind
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 (!'a, !'b) location =
  1. | HypLocation of 'a
  2. | ConclLocation of 'b
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;
  2. mltac_tactic : string;
}
type ml_tactic_entry = {
  1. mltac_name : ml_tactic_name;
  2. mltac_index : int;
}
type glob_constr_and_expr = Genintern.glob_constr_and_expr
type open_constr_expr = unit * Constrexpr.constr_expr
type open_glob_constr = unit * glob_constr_and_expr
type binding_bound_vars = Constr_matching.binding_bound_vars
type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * Pattern.constr_pattern
type !'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
type delayed_open_constr_with_bindings = EConstr.constr Tactypes.with_bindings delayed_open
type delayed_open_constr = EConstr.constr delayed_open
type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
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) option
  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 ('trm Locus.with_occurrences * 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, 'pat) Genredexpr.red_expr_gen * 'nam Locus.clause_expr
  12. | TacChange of 'pat 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 = < constant : 'cst ; dterm : 'dtrm ; level : 'lev ; name : 'nam ; pattern : 'pat ; reference : 'ref ; tacexpr : 'tacexpr ; term : 'trm >
type !'a gen_tactic_arg =
  1. | TacGeneric of 'lev Genarg.generic_argument
  2. | ConstrMayEval of ('trm, 'cst, 'pat) Genredexpr.may_eval
  3. | Reference of 'ref
  4. | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located
  5. | TacFreshId of string Locus.or_var list
  6. | Tacexp of 'tacexpr
  7. | TacPretype of 'trm
  8. | TacNumgoals
constraint 'a = < constant : 'cst ; dterm : 'dtrm ; level : 'lev ; name : 'nam ; pattern : 'pat ; reference : 'ref ; tacexpr : 'tacexpr ; term : 'trm >
and !'a gen_tactic_expr =
  1. | TacAtom of 'a gen_atomic_tactic_expr Loc.located
  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. | TacComplete of 'a gen_tactic_expr
  9. | TacSolve of 'a gen_tactic_expr list
  10. | TacTry of 'a gen_tactic_expr
  11. | TacOr of 'a gen_tactic_expr * 'a gen_tactic_expr
  12. | TacOnce of 'a gen_tactic_expr
  13. | TacExactlyOnce of 'a gen_tactic_expr
  14. | TacIfThenCatch of 'a gen_tactic_expr * 'a gen_tactic_expr * 'a gen_tactic_expr
  15. | TacOrelse of 'a gen_tactic_expr * 'a gen_tactic_expr
  16. | TacDo of int Locus.or_var * 'a gen_tactic_expr
  17. | TacTimeout of int Locus.or_var * 'a gen_tactic_expr
  18. | TacTime of string option * 'a gen_tactic_expr
  19. | TacRepeat of 'a gen_tactic_expr
  20. | TacProgress of 'a gen_tactic_expr
  21. | TacShowHyps of 'a gen_tactic_expr
  22. | TacAbstract of 'a gen_tactic_expr * Names.Id.t option
  23. | TacId of 'n message_token list
  24. | TacFail of global_flag * int Locus.or_var * 'n message_token list
  25. | TacInfo of 'a gen_tactic_expr
  26. | TacLetIn of rec_flag * (Names.lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr
  27. | TacMatch of lazy_flag * 'a gen_tactic_expr * ('p, 'a gen_tactic_expr) match_rule list
  28. | TacMatchGoal of lazy_flag * direction_flag * ('p, 'a gen_tactic_expr) match_rule list
  29. | TacFun of 'a gen_tactic_fun_ast
  30. | TacArg of 'a gen_tactic_arg Loc.located
  31. | TacSelect of Goal_select.t * 'a gen_tactic_expr
  32. | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
  33. | TacAlias of (Names.KerName.t * 'a gen_tactic_arg list) Loc.located
constraint 'a = < constant : 'c ; dterm : 'dtrm ; level : 'l ; name : 'n ; pattern : 'p ; reference : 'r ; tacexpr : 'tacexpr ; term : 't >
and !'a gen_tactic_fun_ast = Names.Name.t list * 'a gen_tactic_expr constraint 'a = < constant : 'c ; dterm : 'dtrm ; level : 'l ; name : 'n ; pattern : 'p ; reference : 'r ; tacexpr : 'te ; term : 't >
type g_nam = Names.lident
type g_dispatch = < constant : g_cst ; dterm : g_trm ; level : Genarg.glevel ; name : g_nam ; pattern : g_pat ; reference : g_ref ; tacexpr : glob_tactic_expr ; term : g_trm >
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 = < constant : r_cst ; dterm : r_trm ; level : Genarg.rlevel ; name : r_nam ; pattern : r_pat ; reference : r_ref ; tacexpr : raw_tactic_expr ; term : r_trm >
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_nam = Names.Id.t
type t_dispatch = < constant : t_cst ; dterm : g_trm ; level : Genarg.tlevel ; name : t_nam ; pattern : t_pat ; reference : t_ref ; tacexpr : unit ; term : t_trm >
type atomic_tactic_expr = t_dispatch gen_atomic_tactic_expr
type raw_red_expr = (r_trm, r_cst, r_pat) Genredexpr.red_expr_gen
type glob_red_expr = (g_trm, g_cst, g_pat) Genredexpr.red_expr_gen
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.Id.t * glob_tactic_expr
  6. | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
  1. | TacticDefinition of Names.lident * raw_tactic_expr
  2. | TacticRedefinition of Libnames.qualid * raw_tactic_expr