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
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